Remark that subst can be interprated as lambdas

spec/doc.tex

@@ -605,6 +605,9 @@ substitution for $x_n$. The following example illustrates this idea:
     \operatorname{subst}([x\mapsto 7, x, x \mapsto g(x)]) &= \{x\mapsto g(x)\}\\
 \end{align*}
 
+Formally, the context can be translated to $\lambda$-abstraction and
+application.  This is discussed in the next section.
+
 \paragraph{Implicit Reordering of Equalities.}
 In addition to the explicit steps, solvers might reorder equalities, i.e.,
 apply symmetry of the equality predicate, without generating steps.