Level:
Lib
Thy
Top
:
1
Hypotheses:
E :
n :
EquivRel(
;x,y.
(x E y))
Conclusion:
(n E MinArg(E n : {0..n
}))
Applied Tactic:
Unfold `infix_ap` 0
Generated subgoals:
1
.
(E n MinArg(E n : {0..n
}))
;x,y.
(x E y))
(n E MinArg(E n : {0..n
}))(E n MinArg(E n : {0..n}))