-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.
+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.