of which is based on lambda-like abstraction, the other of which is based on
Combinatory Logic-like manipulations.
+[WARNING: the mapping from the lambda calculus to Combinatory Logic
+has been changed since the class in which it was presented. It now
+matches the presentation in Barendregt. The revised version is
+cleaner, and more elegant. If you spent a lot of time working to
+understand the original version, there's good news and bad news. The
+bad news is that things have changed. The good news is that the new
+version described the same mapping as before, but does it in a cleaner
+way. That is, the CL term that a given lambda term maps onto hasn't
+changed, only the details of how that CL term gets computed. Sorry if
+the changeup causes any distress!]
+
In order to establish the correspondence, we need to get a bit more
official about what counts as an expression in CL. We'll endow CL
with an infinite stock of variable symbols, just like the lambda