+evaluates to the ordered pair (2, 2). It may be helpful to think of
+a redex in the lambda calculus as a particular sort of `let`
+construction.
+
+ ((\x BODY) ARG) is analogous to
+
+ let x match ARG
+ in BODY
+
+This analogy should be treated with caution. For one thing, our `letrec`
+allowed us to define recursive functions in which the name `x` appeared within
+`ARG`, but we wanted it there to be bound to the very same `ARG`. We're not
+ready to deal with recursive functions in the lambda calculus yet.
+
+For another, we defined `let` in terms of *values*: we said that the variable
+`x` was bound to whatever *value* `ARG` *evaluated to*. At this point, it's
+not clear what the values are in the lambda calculus. We only have expressions.
+(Though there was a suggestive remark earlier about some of the expressions but
+not others being called "value terms".)
+
+So perhaps we should translate `((\x BODY) ARG)` in purely syntactic terms,
+like: "let `x` be replaced by `ARG` in `BODY`"?
+
+Most problematically, in the lambda
+calculus, an abstract such as `(\x (x x))` is perfectly well-formed
+and coherent, but it is not possible to write a `let` expression that
+does not have an `ARG`. That would be like:
+
+ `let x match` *missing*
+ `in x x`
+
+Nevertheless, the correspondence is close enough that it can guide our
+intuition.