Level: Lib Thy Top: 1
Hypotheses:

  1. E :

  2. n :

  3. k :

  4. EquivRel(;x,y.(x E y))

Conclusion:

(n E k) Min{ x | xEn } = Min{ x | xEk }

Applied Tactic: D 0 THENW Auto
Generated subgoals:

1. Min{ x | xEn } = Min{ x | xEk }