+Given the internal structure of the term we are using to represent
+zero, its type must have the form ρ --> σ --> σ for
+some ρ and σ. This type is consistent with term for one,
+but the structure of the definition of one is more restrictive:
+because the first argument (`s`) must apply to the second argument
+(`z`), the type of the first argument must describe a function from
+expressions of type σ to some result type. So we can refine
+ρ by replacing it with the more specific type σ --> τ.
+At this point, the overall type is (σ --> τ) --> σ -->
+σ. Note that this refined type remains compatible with the
+definition of zero. Finally, by examinining the definition of two, we
+see that expressions of type τ must be suitable to serve as
+arguments to functions of type σ --> τ, since the result of
+applying `s` to `z` serves as the argument of `s`. The most general
+way for that to be true is if τ ≡ σ. So at this
+point, we have the overall type of (σ --> σ) --> σ
+--> σ.