≡ (\n s z. s (n s z)) X
~~> \s z. s (X s z)
<~~> succ (\s z. s (X s z)) ; using fixed-point reasoning
-~~> \s z. s ([succ (\s z. s (X s z))] s z)
-~~> \s z. s ([\s z. s ([succ (\s z. s (X s z))] s z)] s z)
-~~> \s z. s (s (succ (\s z. s (X s z))))
+≡ (\n s z. s (n s z)) (\s z. s (X s z))
+~~> \s z. s ((\s z. s (X s z)) s z)
+~~> \s z. s (s (X s z))
</code></pre>
So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
~~> mul 2 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 1)
...
~~> mul 2 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] 0))
-≡ mul 2 (mul 1 (iszero 0 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0))))
+≡ mul 2 (mul 1 (iszero 0 1 (mul 1 ([prefact ((\x. prefact (x x)) (\x. prefact (x x)))] (pred 0)))))
~~> mul 2 (mul 1 1)
~~> mul 2 1
~~> 2