Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
f:
.
n:
. MinArg(f : {0..n
})
(n + 1)
Applied Tactic:
Unfold `min_arg` 0 THEN Auto'
Generated subgoals:
None
f:
. n:. MinArg(f : {0..n
}) 
(n + 1)