Apply 4 suggestion(s) to 1 file(s)

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

spec/rule_list.tex

@@ -1553,8 +1553,9 @@ $k$. & $\Gamma$ & \ctxsep &
 
 \begin{RuleDescription}{bind_let}
   This rule corresponds to the \proofRule{bind} rule for \inlineAlethe{let}.
-  It allows the renaming of the variable bound by the \inlineAlethe{let} step,
-  and rewriting of the substituted term without removing the \inlineAlethe{let}.
+  It allows the renaming of the variables bound by the \inlineAlethe{let} step,
+  the rewriting of the substituted terms, and the rewriting of the body of the 
+  \inlineAlethe{let}, resulting in a new \inlineAlethe{let} term.  
   It has the form
 
 \begin{AletheXS}
@@ -1562,15 +1563,17 @@ $i_1$. & $\Gamma$ & \ctxsep & $t_{1} ≈ s_{1}$ & ($\dots$) \\
 \aletheLineS
 $i_n$. & $\Gamma$ & \ctxsep & $t_{n} ≈ s_{n}$ & ($\dots$) \\
 \aletheLineS
-$j$. & \spctx{$\Gamma, x_1, \dots,  x_n$}
+$j$. & \spctx{$\Gamma, y_1,\dots, y_n,  x_1 \mapsto y_1, \dots ,  x_n \mapsto y_n$}
    & \ctxsep &  $u ≈ u'$ & ($\dots$) \\
 \spsep
 $k$. & $\Gamma$ & \ctxsep &
      $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u) ≈
-      (\lsymb{let}\,x_1~=~s_1,\, \dots,\, x_n~=~s_n\,\lsymb{in}\, u')$
+      (\lsymb{let}\,y_1~=~s_1,\, \dots,\, y_n~=~s_n\,\lsymb{in}\, u')$
      & (\currule{}\;$i_1$, \dots, $i_n$) \\
 \end{AletheXS}
 
+  The variables $y_1, \dots, y_n$ are neither free in $(\lsymb{let}\,x_1 = t_1,\, \dots,\, x_n = t_n\,\lsymb{in}\, u)$ nor, for each $y_i$ different from $x_i$, occur in $\Gamma$.
+
   The premise $i_1, \dots, i_n$ must be in the same subproof as
   the \currule{} step.  If for $t_i≈ s_i$ the $t_i$ and $s_i$
   are syntactically equal, the premise