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