Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

E: . n,k:. EquivRel(;x,y.(x E y)) (n E k) Min{ x | xEn } = Min{ x | xEk }

Applied Tactic: UnivCD THENA Auto
Generated subgoals:

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