-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.
+
+Could we try to build a system for doing Church arithmetic in which
+the type for numbers always manipulated ordered pairs? The problem is
+that the ordered pairs we need here are pairs of numbers. If we tried
+to replace the type for Church numbers with a concrete (simple) type,
+we would have to replace each `X` with the type for Pairs, `(N -> N ->
+N) -> N`. But then we'd have to replace each of these `N`'s with the
+type for Church numbers, `(X -> X) -> X -> X`. And then we'd have to
+replace each of these `X`'s with... ad infinitum. If we had to choose
+a concrete type built entirely from explicit base types, we'd be
+unable to proceed.
+