From 17f0b594a8eb28583ebc804bfef6c9eb2b250751 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Wed, 8 May 2024 11:34:16 -0500
Subject: [PATCH] =?UTF-8?q?Clarifiy=20that=20bind=20can=20work=20on=20?=
 =?UTF-8?q?=E2=88=83=20and=20=E2=88=80?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Addresses https://gitlab.uliege.be/verit/alethe/-/issues/37
---
 spec/changelog.tex |  2 ++
 spec/rule_list.tex | 11 ++++++++---
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/spec/changelog.tex b/spec/changelog.tex
index 5b76a0a..8ce4b70 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 a2b19dd..200fb46 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}
-- 
GitLab