Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
E:T
T
. EquivRel(T;x,y.E[x;y])
(
a:T. [a]{x,y:T//E[x;y]}
x,y:T//E[x;y])
Applied Tactic:
(Unfold `type_inj` 0 ...)
Generated subgoals:
None
T:
. E:T 
T 
. EquivRel(T;x,y.E[x;y]) 
(a:T. [a]{x,y:T//E[x;y]} 
x,y:T//E[x;y])