Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
E:T
T
. EquivRel(T;x,y.x E y)
(
x,y:T. x = y
x = y)
Applied Tactic:
(UnivCD ...a)
Generated subgoals:
1
. x = y
T:
. E:T 
T 
. EquivRel(T;x,y.x E y) 
(x,y:T. x = y x = y)