aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3093.v
blob: f6b4a03f3b6348740db07d827badecc32cb5c1e7 (plain)
1
2
3
4
5
6
Require Import FunctionalExtensionality.

Goal forall y, @f_equal = y.
  intro.
  apply functional_extensionality_dep.
Abort.