let fst = λx:N.λy:N.x in
let snd = λx:N.λy:N.y in
let pair = λx:N.λy:N.λz:N->N->N.z x y in
- let suc = λn:N.λα.λs:α->α.λz:α.s (n [α] s z) in
+ let suc = λn:N.Î\9bα.λs:α->α.λz:α.s (n [α] s z) in
let shift = λp:Pair.pair (suc (p fst)) (p fst) in
let pre = λn:N.n [Pair] shift (pair zero zero) snd in