+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
+calculus, including `x`, `y`, and `z`. In addition, `S`, `K`, and `I`
+are expressions in CL. Finally, `(XY)` is in CL for any CL
+expressions `X` and `Y`. So examples of CL expressions include
+`x`, `(xy)`, `Sx`, `SK`, `(x(SK))`, `(K(IS))`, and so on. When we
+omit parentheses, the assumption will be left associativity, so that
+`XYZ == ((XY)Z)`.
+
+It may seem wierd to allow variables in CL. The reason that is
+necessary is because we're trying to show that every lambda term can
+be translated into an equivalent CL term. Since some lambda terms
+contain free variables, we need to provide a translation for free
+variables. As you might expect, it will turn out that whenever the
+lambda term in question contains no free variables (i.e., is a
+combinator), its translation in CL will also contain no variables.
+
+Assume that for any lambda term T, [T] is the equivalent Combinatory
+Logic term. Then we can define the [.] mapping as follows.
+
+ 1. [a] a
+ 2. [\aX] @a[X]
+ 3. [(XY)] ([X][Y])
+
+ 4. @aa I
+ 5. @aX KX if a is not in X
+ 6. @a(XY) S(@aX)(@aY)
+
+Think of `@aX` as a psuedo-lambda abstract.