-The key to the extra flexibility provided by System F is that we can
-instantiate the `pair` function to return a number, as in the
-definition of `pre`, or we can instantiate it to return an ordered
-pair, as in the definition of the `shift` function. Because we don't
-have to choose a single type for all uses of the pair-building
-function, we aren't forced into a infinite regress of types.
-
+The key to the extra expressive power provided by System F is evident
+in the typing imposed by the definition of `pre`. The variable `n` is
+typed as a Church number, i.e., as `All X . (X->X)->X->X`. The type
+application `n [Pair]` instantiates `n` in a way that allows it to
+manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`. In
+other words, the instantiation turns a Church number into a
+pair-manipulating function, which is the heart of the strategy for
+this version of predecessor.
+
+But of course, the type `Pair` (in this simplified example) is defined
+in terms of Church numbers. If we tried to replace the type for
+Church numbers with a concrete (simple) type, we would have to replace
+each `X` with `(N -> N -> N) -> N`. But then we'd have to replace
+each `N` with `(X -> X) -> X -> X`. And then replace each `X`
+with... ad infinitum. If we had to choose a concrete type built
+entirely from explicit base types, we'd be unable to proceed.
+