-Version 1 type numerals are not a good choice for the simply-typed
-lambda calculus. The reason is that each different numberal has a
-different type! For instance, if zero has type σ, then since
-one is represented by the function `\x.x false 0`, it must have type
-`b --> σ --> σ`, where `b` is the type of a boolean. But
-this is a different type than zero! Because each number has a
-different type, it becomes unbearable to write arithmetic operations
-that can combine zero with one, since we would need as many different
-addition operations as we had pairs of numbers that we wanted to add.
+The Church numerals are well behaved with respect to types. They can
+all be given the type (σ --> σ) --> σ --> σ.