Glorp

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)

succ := λn.λf.λx.f (n f x)
+ := λa.λb.a succ b
* := λa.λb.a (b succ) 0

pair := λa.λb.λf.f a b
fst := λc.c (λa.λb.a)