Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
(
n,k,z.(n
k))
n:
k:
True
Applied Tactic:
ProveOpCombTyping `exp_wf2`
Generated subgoals:
None
(
n,k,z.(n
k)) 
n:
k: 
True