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` and `(+n)` may not be a fixed point for `(*n)` or for
+you found for `succ` and `(+n)` (recall this is shorthand for `\x. add x n`) may not be a fixed point for `(*n)` or for
`(^n)`.