(true x y) := x
(false x y) := y

(pair a b) := \c.(c a b)
(left p) := (p true)
(false p) := (p false)

zero 0 1 x = x

inc n := \0 1 x.{
  initial := (pair true x)
  (on_zero p) := (pair false ((left p 1 0) (right p)))
  (on_one p) := (pair (left p) (1 (right p)))
  
  (n on_zero on_one initial)
}