+ let shift = \p. pair (succ (p fst)) (p fst) in
+ let pred = \n. n shift (pair zero zero) snd in
+
+Note that `shift` takes a pair `p` as argument, but makes use of only
+the first element of the pair. Why does it do that? In order to
+understand what this code is doing, it is helpful to go through a
+sample computation, the predecessor of 3:
+
+ pred 3
+ 3 shift (pair zero zero) snd
+ (\s z.s(s(s z))) shift (pair zero zero) snd
+ shift (shift (shift (\f.f 0 0))) snd
+ shift (shift (pair (succ ((\f.f 0 0) fst)) ((\f.f 0 0) fst))) snd
+ shift (shift (\f.f 1 0)) snd
+ shift (\f. f 2 1) snd
+ (\f. f 3 2) snd
+ snd 3 2
+ 2
+
+At each stage, `shift` sees an ordered pair that contains two numbers
+related by the successor function. It can safely discard the second
+element without losing any information. The reason we carry around
+the second element at all is that when it comes time to complete the
+computation---that is, when we finally apply the top-level ordered
+pair to `snd`---it's the second element of the pair that will serve as
+the final result.