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 THENW Auto THEN D 0 THENW Auto
Generated subgoals:1. (n E k) Min{ x | xEn } = Min{ x | xEk }2. (n E k) Min{ x | xEn } = Min{ x | xEk }