-As you would expect, a term in CL is in normal form when it contains
-no redexes (analogously for head normal form, weak head normal form, etc.)
-
-In order to fully reduce a term, we need to be able to reduce redexes
-that are not at the top level of the term.
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
+Warning: this method for telling whether a term is a redex relies on the accidental fact that the
+one-step reduction of a CL term is never identical to the original
+term. This would not work for the untyped lambda calculus, since
+`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Neither would it work if
+we had chosen some other combinators as primitives (`W W1 W2` reduces to
+`W1 W2 W2`, so if they are all `W`s we'd be in trouble.) We will discuss
+some alternative strategies in other notes.
+
+So far, we've only asked whether a term _is_ a redex, not whether it _contains_ other redexes as subterms. But
+in order to fully reduce a term, we need to be able to reduce redexes
+that are not at the top level of the term. Because we need to process subterms, and because the result after
+processing a subterm may require further processing, the recursive