You need to construct integers with a tuple type, in lambda calculus its: pair = λ x. λ y. λ z. x. y. z Or if you are willing to let pred(0) = 0 then you

You need to construct integers with a tuple type, in lambda calculus its: pair = λ x. λ y. λ z. x. y. z Or if you are willing to let pred(0) = 0 then you can use: pred = λ x. λy. λ z. x . (λ i. λ j. j. i. y (λ k. z) (λ k. k)