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