Sequencing or continuation-passing in pure lambda-calculus


I am trying to solve the following exercise given here.

Consider the following number representation. How to define the addition?

|0| = λx.x |1| = λx.λx.x  ... |n + 1| = λx.|n| 

The successor and predecessor operators are easy to define:

Succ n = λx.n Pred n = n λx.x 

An "obvious" solution for defining the addition is to use the successor operation plus the test for zero together with the fixed point combinator, something like (Y F) for F given below (the operator if and booleans are defined as usual):

F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n)) 

But defining Is0 seems non-trivial. The problem is that a numeral |N| consumes N+1 arguments, and N arguments are simply erased by it. Hence, if I apply such a function, it seems reasonable to stop its application when it becomes clear that the numeral, e.g. is not an identity. I guess it is some sort of continuation, but I cannot imagine how to model it in the pure lambda-calculus. Maybe someone knows any tips that may help?

A sequencing operator can also help to define the addition. If an application of a numeral |m| is delayed until a numeral |n| is applied to all its arguments, the result will be exactly a numeral |n+m|. Maybe there exists a variant of such a sequencing combinator in the pure lambda-calculus?

The answer which is provided by the author of the exercise uses a non-pure operation (namely, IsProcedure which checks whether its argument is a function).