id = ^x.x
if = ^b.^t.^f.b t f
true = ^x.^y.x
false = ^x.^y.y
and = ^p.^q.if p q false
or = ^p.^q.if p true q
not = ^p.if p false true
cons = ^h.^t.^s.s h t
head = ^l.l true
tail = ^l.l false
isnull = ^l.l ^h.^t.false
nil = ^s.true
zero = ^f.^x.x
one = ^f.^x.f x
two = ^f.^x.f (f x)
three = ^f.^x.f (f (f x))
four = ^f.^x.f (f (f (f x)))
five = ^f.^x.f (f (f (f (f x))))
six = ^f.^x.f (f (f (f (f (f x)))))
seven = ^f.^x.f (f (f (f (f (f (f x))))))
eight = ^f.^x.f (f (f (f (f (f (f (f x)))))))
nine = ^f.^x.f (f (f (f (f (f (f (f (f x))))))))
ten = ^f.^x.f (f (f (f (f (f (f (f (f (f x)))))))))
succ = ^n.^f.^x.n f (f x)
add = ^m.^n.^f.^x.m f (n f x)
pred = ^n.tail (n (^p.cons (succ (head p)) (head p)) (cons zero zero))
sub = ^m.^n.n pred m
mul = ^m.^n.^f.m (n f)
exp = ^m.^n.n m
Y = ^f.(^x.f (x x)) (^x.f (x x))
Y_ = ^f.(^x.f (^y.x x y)) (^x.f (^y.x x y))
lenF = ^f.^l.(isnull l) zero (succ (f (tail l)))
len = Y lenF
len_ = Y_ lenF