Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
E:
.
n:
. EquivRel(
;x,y.
(x E y))
(n E Min{ x | xEn })
Applied Tactic:
UnivCD THENW Auto THEN Unfold `min_el` 0
Generated subgoals:
1
.
(n E MinArg(E n : {0..n
}))
E:
. n:. EquivRel(;x,y.
(x E y)) 
(n E Min{ x | xEn })(n E MinArg(E n : {0..n
}))