The key to the extra expressive power provided by System F is evident
in the typing imposed by the definition of `pred`. The variable `n`
-is typed as a Church number, i.e., as `N ≡ ∀α.(α->α)->α->α`.
+is typed as a Church number, i.e., as <code>N ≡ ∀α.(α->α)->α->α</code>.
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 certain