Level:
Lib
Thy
Top
:
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:
BLemma `iff_imp_equal_bool` THENA Auto
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)