Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
f,n,z.MinArg(f : {0..n
}))
f:(
)
n:
True
(n + 1)
Applied Tactic:
ProveOpCombTyping `min_arg_wf`
Generated subgoals:
None
(
f,n,z.MinArg(f : {0..n
})) 
f:(
) n: 
True (n + 1)