This allows you to extract large church numbers from abstract's algorithm. It is just a very efficient implementation of natToBinary : Nat -> Bits
.
U= x.(x x)
8= s.z.(s (s (s (s (s (s (s (s z))))))))
19= s.z.(s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))))))
succ=