1. Find a fixed point `X` for the succ function:
H := \f.succ(ff)
X := HH
== (\f.succ(ff)) H
~~> succ(HH)
So `succ(HH) <~~> succ(succ(HH))`.
2. Prove that `add 1 X <~~> X`:
add 1 X == (\mn.m succ n) 1 X
~~> 1 succ X
== (\fz.fz) succ X
~~> succ X
What about `add 2 X`?
add 2 X == (\mn.m succ n) 2 X
~~> 2 succ X
== (\fz.f(fz)) succ X
~~> succ (succ X)
So `add n X <~~> X` for all (finite) natural numbers `n`.