+#Q. So `Y` applied to `succ` returns a number that is not finite!#
+
+A. Yes! Let's see why it makes sense to think of `Y succ` as a Church
+numeral:
+
+ [same definitions]
+ succ X
+ = (\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))))
+
+So `succ X` looks like a numeral: it takes two arguments, `s` and `z`,
+and returns a sequence of nested applications of `s`...
+
+You should be able to prove that `add 2 (Y succ) <~~> Y succ`,
+likewise for `mult`, `minus`, `pow`. What happens if we try `minus (Y
+succ)(Y succ)`? What would you expect infinity minus infinity to be?
+(Hint: choose your evaluation strategy so that you add two `s`s to the
+first number for every `s` that you add to the second number.)
+
+This is amazing, by the way: we're proving things about a term that
+represents arithmetic infinity.
+
+It's important to bear in mind the simplest term in question is not
+infinite:
+
+ Y succ = (\f. (\x. f (x x)) (\x. f (x x))) (\n s z. s (n s z))
+
+The way that infinity enters into the picture is that this term has
+no normal form: no matter how many times we perform beta reduction,
+there will always be an opportunity for more beta reduction. (Lather,
+rinse, repeat!)
+
+