succ
- n: Nat
: Nat

~λP λsucc λzero (succ n)