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