Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
E:T
T
.
s,t:T. EquivRel(T;x,y.
(x E y))
(s E t)
E s = E t
Applied Tactic:
UnivCD THENW Auto THEN Ext THENA Auto
Generated subgoals:
1
. E s x = E t x
T:
. E:T 
T 
. s,t:T. EquivRel(T;x,y.
(x E y)) 
(s E t) E s = E t