Nat = ∀α::*.α → (α → α) → α;

zero = Λα::*.λz:α.λs:α → α.z;

succ = λn:Nat.Λα::*.λz:α.λs:α → α.s (n [α] z s);

add = λm:Nat.λn:Nat.m [Nat] n succ;
