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