Level:
Lib
Thy
Top
:
1
1
Hypotheses:
E :
n :
k :
EquivRel(
;x,y.
(x E y))
(n E k)
Conclusion:
Min{ x | xEn } = Min{ x | xEk }
Applied Tactic:
BLemma `min_el_unique` THEN Auto
Generated subgoals:
None
;x,y.
(x E y))(n E k)
Min{ x | xEn } = Min{ x | xEk }