Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
E:T
T
. EquivRel(T;x,y.E[x;y])
(
a,b:T. a = b
E[a;b])
Applied Tactic:
GenUnivCD THENA Auto
Generated subgoals:
1
.
E[a;b]
2
. a = b
T:
. E:T 
T 
. EquivRel(T;x,y.E[x;y]) 
(a,b:T. a = b 
E[a;b])E[a;b]