+ let shift = \p. p (\a b. pair (succ a) a)
+ let pred = \n. n shift (pair zero zero) snd in
+
+Note that `shift` applies its argument p ("p" for "pair") to a
+function that ignores its second argument---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 (\s z.s(s(s z)))
+ (\s z.s(s(s z))) (\n.n shift (\f.f 0 0) snd)
+ shift (shift (shift (\f.f 0 0))) snd
+ shift (shift ((\f.f 0 0) (\a b.pair(succ a) a))) snd
+ shift (shift (\f.f 1 0)) snd
+ shift (\f. f 2 1) snd
+ (\f. f 3 2) snd
+ 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.