to use this object to model arithmetic infinity. For instance,
depending on implementation details, it might happen that `leq n ΞΎ` is
true for all (finite) natural numbers `n`. However, the fixed point
-you found for `succ` may not be a fixed point for `mult n` or for
-`exp n`.
+you found for `succ` and `(+n)` may not be a fixed point for `(*n)` or for
+`(^n)`.
## Mutually-recursive functions ##