diff --git a/spec/doc.tex b/spec/doc.tex index d16a68b82c1142a7c23071a11f03bc53c42ab6da..6505e3fcc86e1decac6fa4a9e966a4c1f6d3134d 100644 --- a/spec/doc.tex +++ b/spec/doc.tex @@ -555,7 +555,8 @@ Every context $\Gamma$ induces a capture-avoiding substitution $\subst(\Gamma)$. If $\Gamma$ is the empty list, $\subst(\Gamma)$ is the empty substitution, i.e, the identity function. -The first case fixes $x_n$ and allows the context to shadow a previously defined +Otherwise, if $\Gamma$ ends with variable $x_n$, this fixes the variable +and allows the context to shadow a previously defined substitution for $x_n$: \[ \subst([c_1,\dots, c_{n-1}, x_n])