Level:
Lib
Thy
Top
:
1
1
Hypotheses:
T :
E : T
T
s : T
t : T
EquivRel(T;x,y.
(x E y))
(s E t)
x : T
Conclusion:
(E s x)
(E t x)
Applied Tactic:
D 5 THEN D 6
Generated subgoals:
1
.
(E s x)
(E t x)
T 
(x E y))(s E t)
(E s x) 
(E t x)(E s x) (E t x)