-(Various, slightly differing translation schemes from combinatory logic to the
-lambda calculus are also possible. These generate different metatheoretical
-correspondences between the two calculii. Consult Hindley and Seldin for
-details. Also, note that the combinatorial proof theory needs to be
+Finally, the last rule says that if the body of an abstract is itself an abstract, translate the inner abstract first, and then do the outermost. (Since the translation of `[\b. M]` will have eliminated any inner lambdas, we can be sure that we won't end up applying rule 6 again in an infinite loop.)
+
+Persuade yourself that if the original lambda term contains no free variables --- i.e., is a combinator --- then the translation will consist only of `S`, `K`, and `I` (plus parentheses).
+
+(Fussy note: this translation algorithm builds intermediate expressions that combine lambdas with primitive combinators. For instance, the translation of our boolean `false` (`\x y. y`) is `[\x [\y. y]] = [\x. I] = KI`. In the intermediate stage, we have `\x. I`, which has a combinator in the body of a lambda abstract. It's possible to avoid this if you want to, but it takes some careful thought. See, e.g., Barendregt 1984, page 156.)
+
+Various, slightly differing translation schemes from Combinatory Logic to the
+Lambda Calculus are also possible. These generate different metatheoretical
+correspondences between the two calculi. Consult Hindley and Seldin for
+details.
+
+Also, note that the combinatorial proof theory needs to be