Theorem:
succ^0 = I = \nfx. n f x
succ^2k = \nfx. n (succ^(2k-1) n f) x
succ^(2k+1) = \nfx. f (succ^(2k) n f x)
Proof:
succ^(2k+1) = succ^2k succ
= \fx. succ (succ^(2k-1) succ f) x
= \nfx. succ (succ^(2k) n) f x
= \nfx. S (\u. S (K u)) (succ^(2k) n) f x
= \nfx. S (K f) (succ^(2k) n f) x
= \nfx. f (succ^(2k) n f) x
succ^(2k) = succ^(2k-1) succ
= \fx. f (succ^(2k-2) succ f x)
= \nfx. n (succ^(2k-1) n f) x