Assume Ω has type τ, and `\x.xx` has type σ. Then
because `\x.xx` takes an argument of type σ and returns
-something of type τ, `\x.xx` must also have type `σ -->
-τ`. By repeating this reasoning, `\x.xx` must also have type
-`(σ --> τ) --> τ`; and so on. Since variables have
+something of type τ, `\x.xx` must also have type σ -->
+τ. By repeating this reasoning, `\x.xx` must also have type
+(σ --> τ) --> τ; and so on. Since variables have
finite types, there is no way to choose a type for the variable `x`
that can satisfy all of the requirements imposed on it.
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 `false`
-has type τ --> τ --> &tau, for some τ. Since one is
+has type τ --> τ --> τ, for some τ. Since one is
represented by the function `\x.x false 0`, one must have type (τ
---> τ --> &tau) --> &sigma --> σ. But this is a different
+--> τ --> τ) --> σ --> σ. But this is a different
type than zero! Because each number has a different type, it becomes
impossible to write arithmetic operations that can combine zero with
one. We would need as many different addition operations as we had