id ::= \x -> x pred ::= succ \x -> x Nat ::= zero | succ Nat nat \z \s ::= zero -> z | succ \n -> s (nat z s n) Nat + Nat :: Nat \x + \y = nat x succ y Nat - Nat :: Nat \x - \y = nat x (pred | id) y