+ ANSWER: Prove that `add X 1 <~~> X`:
+
+ add X 1 == (\m n. n succ m) X 1
+ ~~> 1 succ X
+ == (\s z. s z) succ X
+ ~~> succ X
+
+ Which by the previous problem is convertible with `X`. (In particular, `X ~~> succ X`.) What about `add X 2`?
+
+ add X 2 == (\m n. n succ m) X 2
+ ~~> 2 succ X
+ == (\s z. s (s z)) succ X
+ ~~> succ (succ X)
+
+ And we know the inner term will be convertible with `X`, and hence we get that the whole result is convertible with `succ X`. Which we already said is convertible with `X`. We can readily see that `add X n <~~> X` for all (finite) natural numbers `n`.
+
+