test-suite/bugs/closed/shouldsucceed/2262.v


1
2
3
4
5
6
7
8
9
10
11


Generalizable Variables A.
Class Test A := { test : A }.

Lemma mylemma : forall `{Test A}, test = test.
Admitted. (* works fine *)

Definition mylemma' := forall `{Test A}, test = test.
About mylemma'.