-That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
-the `\w` protects the redex in the body from reduction.
-(A redex is a subform ...(\xM)N..., i.e., something that can be the
-target of reduction.)
+That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
+`\u.z`, because the `\u` protects the redex in the body from
+reduction. (In this context, a "redex" is a part of a term that matches
+the pattern `...((\xM)N)...`, i.e., something that can potentially be
+the target of beta reduction.)