From 961e2414f9b31c2c932bb2b9edf1a5938ea71b19 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 9 Jan 2024 19:30:59 +0100
Subject: Fix a typo and make small improvement noted during lecture on
 2024-01-09.

---
 transp-inf110-03-quantif.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 5c69859..e0e44b9 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -344,7 +344,7 @@ $\bot$
 \\\hline
 $\forall$
 &$\inferrule{\Gamma, {\color{mydarkgreen}v:I}\vdash Q}{\Gamma\vdash \forall (v:I).\, Q}$ ($v$ \alert{frais})
-&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall (v:I).\, Q}{\Gamma\vdash Q[v\backslash t]}$
+&$\inferrule{\Gamma\vdash \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[v\backslash t]}$
 \\\hline
 $\exists$
 &$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[v\backslash t]}{\Gamma\vdash \exists (v:I).\, Q}$
@@ -401,7 +401,7 @@ type $I$, on notera $ft$ la preuve de $Q[v\backslash t]$ {\footnotesize
 {\footnotesize (\textbf{N.B.} on n'explique pas comment le « terme
   d'individu » $t$ est formé.)}
 \[
-\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
+\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]}
 \]
 
 \medskip
@@ -481,7 +481,7 @@ $\bot$
 \\\hline
 $\forall$
 &\scalebox{0.80}{$\inferrule{\Gamma, v:I\vdash s:Q}{\Gamma\vdash \lambda(v:I).\,s\;:\;\forall (v:I).\, Q}$}
-&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash f \;:\; \forall (v:I).\, Q}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
+&\scalebox{0.80}{$\inferrule{\Gamma\vdash f \;:\; \forall (v:I).\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash ft \;:\; Q[v\backslash t]}$}
 \\\hline
 $\exists$
 &\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$}
@@ -855,7 +855,7 @@ $\bot$
 \\\hline
 $\forall$
 &$\inferrule{\Gamma, {\color{mydarkgreen}x:I}\vdash Q}{\Gamma\vdash \forall x.\, Q}$ ($x$ \alert{frais})
-&$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash \forall x.\, Q}{\Gamma\vdash Q[x\backslash t]}$
+&$\inferrule{\Gamma\vdash \forall x.\, Q\\{\color{gray}\Gamma\vdash t:I}}{\Gamma\vdash Q[x\backslash t]}$
 \\\hline
 $\exists$
 &$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash Q[x\backslash t]}{\Gamma\vdash \exists x.\, Q}$
@@ -1420,7 +1420,7 @@ différent : $A_0 \rightarrow (\prod_n\,(A_n\rightarrow A_{n+1}))
 On peut souvent s'en faire une idée d'après son type, p.ex. :
 \begin{itemize}
 \item La commutativité de la multiplication $\forall m.\forall
-  m.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un
+  n.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un
   témoignage d'égalité de $m\times n$ et $n\times m$ (c'est-à-dire en
   fait $m\times n$ calculé de deux manières différentes).
 \item La preuve de $\forall n. (n=0 \lor \neg n=0)$ donnée
-- 
cgit v1.2.3