# Reducing Kleene's predecessor for Church numerals

I am trying to "reinvent" Kleene's predecessor myself. The following code snippet should be self-explanatory. The idea is to make a 2-tuple and count up from zero, i.e. lambda f: lambda x: x, as described in this article:

#!/usr/bin/env python3

NULL = lambda x: x
ZERO = lambda f: lambda x: x

TRUE = lambda T: lambda F: T(NULL)
FALSE = lambda T: lambda F: F(NULL)
IF_ELSE = lambda cond: lambda T: lambda F: cond(T)(F)
IS_ZERO = lambda n: n(lambda _: FALSE)(TRUE)

ADD1 = lambda n: lambda f: lambda x: f(n(f)(x))

MakePair = lambda first: lambda second: lambda cond: IF_ELSE(cond)(lambda x: first)(lambda x: second)
First = lambda pair: pair(TRUE)
Second = lambda pair: pair(FALSE)
Trans = lambda pair: lambda cond: IF_ELSE(cond)(lambda x: Second(pair))(lambda x: ADD1(Second(pair)))
SUB1 = lambda n: First(n(Trans)(MakePair(ZERO)(ZERO)))

if __name__ == '__main__':
print(SUB1(THREE)(lambda x: x + 1)(0))
print(SUB1(FIVE)(lambda x: x + 1)(0))


In the end, the linked article notes that

It is then straightforward but tedious to expand all of the short-hand expressions above, and reduce the resulting expression to normal form. This results in the standard magical encoding of predecessor.

I assume the normal form of Kleene's predecessor looks like this:

pred = lambda n: lambda f: lambda x: n (lambda g: lambda h: h (g (f))) (lambda y: x) (lambda x: x)


However, after applying a series of expansion and $$\beta$$-reduction, I ended up with this:

SUB1 = lambda n: n(lambda pair: lambda cond: cond(lambda x: pair(lambda T: lambda F: F(NULL)))(lambda x: lambda f: lambda x: f((pair(lambda T: lambda F: F(NULL)))(f)(x))))(lambda _: lambda f: lambda x: x)(lambda T: lambda F: T(lambda x: x))


Question:

How do I reduce my SUB1 function to pred? I don't think we can go further with only $$\beta$$-reduction, and there must be some advanced reduction techniques unknown to me.

A step-by-step solution would be greatly appreciated. Note that this is not a homework problem though; I am doing the exercise just for fun.