From 4dedd4ecaca211bb86ff8a363dd2f1d1c848f813 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Wed, 8 May 2024 11:11:34 -0500
Subject: [PATCH] Fix typo in forall_inst

Adresses https://gitlab.uliege.be/verit/alethe/-/issues/35
---
 spec/rule_list.tex | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 528e776..a2b19dd 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -593,8 +593,10 @@ $i$. & \ctxsep &
 $\neg (\forall x_1, \dots, x_n. P) \lor P[x_1\mapsto t_1]\dots[x_n\mapsto t_n]$
  & \currule\, [$(x_{k_1}, t_{k_1})$, $\dots$, $(x_{k_n}, t_{k_n})$] \\
 \end{AletheX}
-where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_i$ and
-$k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
+
+\noindent
+where $k_1, \dots, k_n$ is a permutation of $1, \dots, n$ and $x_{k_i}$ and
+$t_{k_i}$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
 \inlineAlethe{(:= xki tki)}.
 \end{RuleDescription}
 
@@ -603,6 +605,8 @@ $k_i$ have the same sort. The arguments $(x_{k_i}, t_{k_i})$ are printed as
 \begin{AletheXS}
 $j$. & \ctxsep  & $\Gamma$  & $t_1 ≈ t_2 $ & \currule \\
 \end{AletheXS}
+
+\noindent
 where, if $\sigma = \subst(\Gamma)$,
 the terms $t_1\sigma$ and $t_2$ are
 syntactically equal up to  renaming of
-- 
GitLab