diff --git a/spec/changelog.tex b/spec/changelog.tex
index 5b76a0a765caec94c27f64e52d296970999e8d45..8ce4b70359e079170a0426884bdac3fbe2f72e95 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -21,6 +21,8 @@ Clarifications and corrected errors:
 \begin{itemize}
   \item Clarify that the \texttt{:args} annotation in \texttt{anchor} can be
         omitted if the list is empty.
+  \item Clarify that \proofRule{bind} can work on existential and universal
+        quantifiers.
   \item Fix mistake in proof grammar.  It now uses the \texttt{context\_annotation}
         non-terminal in the rule for the \texttt{anchor} command.
   \item Fix the example of \proofRule{onepoint}.
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index a2b19ddd58e41b3f56eb653f79374fc37daf4aff..200fb46d0a9316e88507582a167e7e89693e1c1a 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -551,11 +551,14 @@ $j$. & \spctx{ $\Gamma, y_1,\dots, y_n,  x_1 \mapsto y_1, \dots ,  x_n \mapsto y
    & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
    \spsep
 $k$. & $\Gamma$ & \ctxsep &
-    $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
+    $Q x_1, \dots, x_n.\varphi ≈ Q y_1, \dots, y_n. \varphi'$
      & \currule{} \\
 \end{AletheXS}
-  where the variables $y_1, \dots, y_n$ are neither free in $\forall x_1,
-  \dots, x_n.\varphi$ nor occur in $\Gamma$.
+
+\noindent
+where $Q \in \{\forall, \exists\}$,
+and the variables $y_1, \dots, y_n$ are neither free in $Q x_1,
+\dots, x_n.\varphi$ nor occur in $\Gamma$.
 \end{RuleDescription}
 
 \begin{RuleDescription}{sko_ex}
@@ -569,6 +572,8 @@ $j$. &
    \spsep
 $k$. & $\Gamma$ & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \end{AletheXS}
+
+\noindent
 where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
 x_n. \varphi)$.
 \end{RuleDescription}