-(Various, slightly differing translation schemes from combinatory logic to the
-lambda calculus are also possible. These generate different metatheoretical
+The fifth rule deals with an abstract whose body is an application: the `S` combinator takes its next argument (which will fill the role of the original variable a) and copies it, feeding one copy to the translation of \a.M, and the other copy to the translation of \a.N. This ensures that any free occurrences of a inside M or N will end up taking on the appropriate value.
+
+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 not have any lambdas in it, 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 expressions that combine lambdas with 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 mixes primitive combinators 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