Better use of mathpartir.

1 files changed, 88 insertions, 88 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index ae52265..64f597f 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -923,16 +923,16 @@ de type $\tau$ dans le contexte $\Gamma$ ».
 Les trois règles de typage du $\lambda$CST :
 
 \[
-\inferrule*[left=\llap{Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma}
+\inferrule*[Left={Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma}
 \]
 
 \[
-\inferrule*[left=\llap{App},sep=4em]{\Gamma \vdash P:\sigma\to\tau\\ \Gamma
+\inferrule*[Left={App},sep=4em]{\Gamma \vdash P:\sigma\to\tau\\ \Gamma
   \vdash Q:\sigma}{\Gamma \vdash PQ:\tau}
 \]
 
 \[
-\inferrule*[left=\llap{Abs}]{\Gamma, v:\sigma \vdash E:\tau}{\Gamma
+\inferrule*[Left={Abs}]{\Gamma, v:\sigma \vdash E:\tau}{\Gamma
   \vdash \lambda(v:\sigma).E : \sigma\to\tau}
 \]
 
@@ -957,17 +957,17 @@ est un terme de type $(\beta\to\alpha\to\gamma) \to
 
 {\footnotesize
 \[
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{App}]{
-\inferrule*[left=\llap{App}]{
-\inferrule*[left=\llap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma}
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={App}]{
+\inferrule*[Left={App}]{
+\inferrule*[Left={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash f : \beta\to\alpha\to\gamma}
 \\
-\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta}
+\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash y : \beta}
 }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash fy : \alpha\to\gamma}
 \\
-\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha}
+\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle f:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle x:\alpha,y:\beta\\ \end{array}$} \vdash x : \alpha}
 }{f:\beta\to\alpha\to\gamma, x:\alpha, y:\beta \vdash fyx : \gamma}
 }{f:\beta\to\alpha\to\gamma, x:\alpha \vdash \lambda(y:\beta). fyx : \beta\to\gamma}
 }{f:\beta\to\alpha\to\gamma \vdash \lambda(x:\alpha). \lambda(y:\beta). fyx : \alpha\to\beta\to\gamma}
@@ -1121,17 +1121,17 @@ dont on n'a donné que les types et les règles appliquées ?
 
 {\footnotesize
 \[
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{Abs}]{
-\inferrule*[left=\llap{App}]{
-\inferrule*[left=\llap{App}]{
-\inferrule*[left=\llap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta\to\alpha\to\gamma}
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={Abs}]{
+\inferrule*[Left={App}]{
+\inferrule*[Left={App}]{
+\inferrule*[Left={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta\to\alpha\to\gamma}
 \\
-\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta}
+\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \beta}
 }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha\to\gamma}
 \\
-\inferrule*[right=\rlap{Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha}
+\inferrule*[Right={Var}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle \textbf{?}:\beta\to\alpha\to\gamma,\\ \scriptscriptstyle \textbf{?}:\alpha,\textbf{?}:\beta\\ \end{array}$} \vdash \textbf{?} : \alpha}
 }{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha, \textbf{?}:\beta \vdash \textbf{?} : \gamma}
 }{\textbf{?}:\beta\to\alpha\to\gamma, \textbf{?}:\alpha \vdash \textbf{?} : \beta\to\gamma}
 }{\textbf{?}:\beta\to\alpha\to\gamma \vdash \textbf{?} : \alpha\to\beta\to\gamma}
@@ -1444,13 +1444,13 @@ de $\land$, etc.) :
 {\footnotesize
 \[
 \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\land$Int}]{
-\inferrule*[left=\llap{$\land$Élim$_2$}]{
-\inferrule*[left=\llap{Ax}]{ }{A\land B \vdash A\land B}
+\inferrule*[Left={$\land$Int}]{
+\inferrule*[Left={$\land$Élim$_2$}]{
+\inferrule*[Left={Ax}]{ }{A\land B \vdash A\land B}
 }{A\land B \vdash B}
 \\
-\inferrule*[right=\rlap{$\land$Élim$_1$}]{
-\inferrule*[right=\rlap{Ax}]{ }{A\land B \vdash A\land B}
+\inferrule*[Right={$\land$Élim$_1$}]{
+\inferrule*[Right={Ax}]{ }{A\land B \vdash A\land B}
 }{A\land B \vdash A}
 }{A\land B \vdash B\land A}
 }{\vdash A\land B \Rightarrow B\land A}
@@ -1462,15 +1462,15 @@ de $\land$, etc.) :
 {\footnotesize
 \[
 \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\lor$Élim}]{
-\inferrule*[left=\llap{Ax}]{ }{A\lor B \vdash A\lor B}
+\inferrule*[Left={$\lor$Élim}]{
+\inferrule*[Left={Ax}]{ }{A\lor B \vdash A\lor B}
 \\
 \inferrule*[right={$\lor$Int$_2$}]{
-\inferrule*[right=\rlap{Ax}]{ }{A\lor B,A \vdash A}
+\inferrule*[Right={Ax}]{ }{A\lor B,A \vdash A}
 }{A\lor B,A \vdash B\lor A}
 \\
-\inferrule*[right=\rlap{$\lor$Int$_1$}]{
-\inferrule*[right=\rlap{Ax}]{ }{A\lor B,B \vdash B}
+\inferrule*[Right={$\lor$Int$_1$}]{
+\inferrule*[Right={Ax}]{ }{A\lor B,B \vdash B}
 }{A\lor B,B \vdash B\lor A}
 }{A\lor B \vdash B\lor A}
 }{\vdash A\lor B \Rightarrow B\lor A}
@@ -1492,13 +1492,13 @@ pour un gain de place) :
 {\footnotesize
 \[
 \inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\land$Int}]{
-\inferrule*[left=\llap{$\land$Élim$_2$}]{
-\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
+\inferrule*[Left={$\land$Int}]{
+\inferrule*[Left={$\land$Élim$_2$}]{
+\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
 }{B}
 \\
-\inferrule*[right=\rlap{$\land$Élim$_1$}]{
-\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
+\inferrule*[Right={$\land$Élim$_1$}]{
+\inferrule*[Right={\textcolor{mydarkgreen}{$u$}}]{ }{A\land B}
 }{A}
 }{B\land A}
 }{A\land B \Rightarrow B\land A}
@@ -1510,15 +1510,15 @@ pour un gain de place) :
 {\footnotesize
 \[
 \inferrule*[left={$\Rightarrow$Int(\textcolor{mydarkgreen}{$u$})},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\lor$Élim(\textcolor{mydarkgreen}{$v$},\textcolor{mydarkgreen}{$v'$})}]{
-\inferrule*[left=\llap{\textcolor{mydarkgreen}{$u$}}]{ }{A\lor B}
+\inferrule*[Left={$\lor$Élim(\textcolor{mydarkgreen}{$v$},\textcolor{mydarkgreen}{$v'$})}]{
+\inferrule*[Left={\textcolor{mydarkgreen}{$u$}}]{ }{A\lor B}
 \\
 \inferrule*[right={$\lor$Int$_2$}]{
-\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v$}}]{ }{A}
+\inferrule*[Right={\textcolor{mydarkgreen}{$v$}}]{ }{A}
 }{B\lor A}
 \\
-\inferrule*[right=\rlap{$\lor$Int$_1$}]{
-\inferrule*[right=\rlap{\textcolor{mydarkgreen}{$v'$}}]{ }{B}
+\inferrule*[Right={$\lor$Int$_1$}]{
+\inferrule*[Right={\textcolor{mydarkgreen}{$v'$}}]{ }{B}
 }{B\lor A}
 }{B\lor A}
 }{A\lor B \Rightarrow B\lor A}
@@ -2009,17 +2009,17 @@ $(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ :
 
 {\footnotesize
 \[
-\inferrule*[left=\llap{$\Rightarrow$Int}]{
-\inferrule*[left=\llap{$\Rightarrow$Int}]{
-\inferrule*[left=\llap{$\Rightarrow$Int}]{
-\inferrule*[left=\llap{$\Rightarrow$Élim}]{
-\inferrule*[left=\llap{$\Rightarrow$Élim}]{
-\inferrule*[left=\llap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C }
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Int}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={$\Rightarrow$Élim}]{
+\inferrule*[Left={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C }
 \\
-\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B }
+\inferrule*[Right={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B }
 }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A \Rightarrow C }
 \\
-\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A }
+\inferrule*[Right={Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A }
 }{B \Rightarrow A \Rightarrow C , A , B  \vdash C }
 }{B \Rightarrow A \Rightarrow C , A  \vdash B \Rightarrow C }
 }{B \Rightarrow A \Rightarrow C  \vdash A \Rightarrow B \Rightarrow C }
@@ -2076,13 +2076,13 @@ de $A\land B \Rightarrow B\land A$
 {\footnotesize
 \[
 \inferrule*[left={Abs},right=\hphantom{Abs}]{
-\inferrule*[left=\llap{Pair}]{
-\inferrule*[left=\llap{Proj$_2$}]{
-\inferrule*[left=\llap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
+\inferrule*[Left={Pair}]{
+\inferrule*[Left={Proj$_2$}]{
+\inferrule*[Left={Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
 }{u:\alpha\times \beta \vdash \pi_2 u:\beta}
 \\
-\inferrule*[right=\rlap{Proj$_1$}]{
-\inferrule*[right=\rlap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
+\inferrule*[Right={Proj$_1$}]{
+\inferrule*[Right={Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
 }{u:\alpha\times \beta \vdash \pi_1 u:\alpha}
 }{u:\alpha\times \beta \vdash \langle \pi_2 u, \pi_1 u\rangle:\beta\times \alpha}
 }{\vdash \lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle : \alpha\times \beta \rightarrow \beta\times \alpha}
@@ -2187,15 +2187,15 @@ de $A\lor B \Rightarrow B\lor A$
 {\footnotesize
 \[
 \inferrule*[left={Abs},right=\hphantom{Int}]{
-\inferrule*[left=\llap{Match}]{
-\inferrule*[left=\llap{Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta}
+\inferrule*[Left={Match}]{
+\inferrule*[Left={Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta}
 \\
 \inferrule*[right={Inj$_2$}]{
-\inferrule*[right=\rlap{Var}]{ }{\ldots,v:\alpha \vdash v:\alpha}
+\inferrule*[Right={Var}]{ }{\ldots,v:\alpha \vdash v:\alpha}
 }{{\scriptstyle\cdots} \vdash \iota_2^{(\beta,\alpha)} v : \beta+\alpha}
 \\
-\inferrule*[right=\rlap{Inj$_1$}]{
-\inferrule*[right=\rlap{Var}]{ }{\ldots,v':\beta \vdash v':\beta}
+\inferrule*[Right={Inj$_1$}]{
+\inferrule*[Right={Var}]{ }{\ldots,v':\beta \vdash v':\beta}
 }{{\scriptstyle\cdots} \vdash \iota_1^{(\beta,\alpha)} v' : \beta+\alpha}
 }{u:\alpha+\beta \vdash (\texttt{match~} u\texttt{~with~}\iota_1
   v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \beta+\alpha}
@@ -2738,20 +2738,20 @@ $\bot$
 
 On reprend les mêmes exemples que dans le
 transp. \ref{example-propositional-proofs} :
-\vskip-5ex\leavevmode
+\vskip-2ex\leavevmode
 \begin{center}
 \begin{tabular}{c|c}
 %
 {\footnotesize
 $
 \inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\land$R}]{
-\inferrule*[left=\llap{$\land$L$_2$}]{
-\inferrule*[left=\llap{Ax}]{ }{B \vdash B}
+\inferrule*[Left={$\land$R}]{
+\inferrule*[Left={$\land$L$_2$}]{
+\inferrule*[Left={Ax}]{ }{B \vdash B}
 }{A\land B \vdash B}
 \\
-\inferrule*[right=\rlap{$\land$L$_1$}]{
-\inferrule*[right=\rlap{Ax}]{ }{A \vdash A}
+\inferrule*[Right={$\land$L$_1$}]{
+\inferrule*[Right={Ax}]{ }{A \vdash A}
 }{A\land B \vdash A}
 }{A\land B \vdash B\land A}
 }{\vdash A\land B \Rightarrow B\land A}
@@ -2761,13 +2761,13 @@ $
 {\footnotesize
 $
 \inferrule*[left={$\Rightarrow$R},right=\hphantom{Int}]{
-\inferrule*[left=\llap{$\lor$L}]{
-\inferrule*[left=\llap{$\lor$R$_2$}]{
-\inferrule*[left=\llap{Ax}]{ }{A \vdash A}
+\inferrule*[Left={$\lor$L}]{
+\inferrule*[Left={$\lor$R$_2$}]{
+\inferrule*[Left={Ax}]{ }{A \vdash A}
 }{A \vdash B\lor A}
 \\
-\inferrule*[right=\rlap{$\lor$R$_1$}]{
-\inferrule*[right=\rlap{Ax}]{ }{B \vdash B}
+\inferrule*[Right={$\lor$R$_1$}]{
+\inferrule*[Right={Ax}]{ }{B \vdash B}
 }{B \vdash B\lor A}
 }{A\lor B \vdash B\lor A}
 }{\vdash A\lor B \Rightarrow B\lor A}
@@ -2783,16 +2783,16 @@ Et que dans le transp. \ref{example-proposition-proof-with-implication} :
 \vskip-2ex
 {\footnotesize
 \[
-\inferrule*[left=\llap{$\Rightarrow$R}]{
-\inferrule*[left=\llap{$\Rightarrow$R}]{
-\inferrule*[left=\llap{$\Rightarrow$R}]{
-\inferrule*[left=\llap{$\Rightarrow$L}]{
-\inferrule*[left=\llap{Ax}]{ }{A, B \vdash B }
+\inferrule*[Left={$\Rightarrow$R}]{
+\inferrule*[Left={$\Rightarrow$R}]{
+\inferrule*[Left={$\Rightarrow$R}]{
+\inferrule*[Left={$\Rightarrow$L}]{
+\inferrule*[Left={Ax}]{ }{A, B \vdash B }
 \\
-\inferrule*[right=\rlap{$\Rightarrow$L}]{
-\inferrule*[left=\llap{Ax}]{ }{A , B  \vdash A }
+\inferrule*[Right={$\Rightarrow$L}]{
+\inferrule*[Left={Ax}]{ }{A , B  \vdash A }
 \\
-\inferrule*[right=\rlap{Ax}]{ }{C , A , B  \vdash C  }
+\inferrule*[Right={Ax}]{ }{C , A , B  \vdash C  }
 }{A \Rightarrow C , A , B  \vdash C }
 }{B \Rightarrow A \Rightarrow C , A , B  \vdash C }
 }{B \Rightarrow A \Rightarrow C , A  \vdash B \Rightarrow C }
@@ -2881,10 +2881,10 @@ Calcul des séquents&Déduction naturelle\\\hline
 $\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash M\\\Gamma,P\vdash R}{\Gamma,M\Rightarrow P\vdash R}$
 &
 $\inferrule*[left=$\Rightarrow$Élim]{
-\inferrule*[left=\llap{$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R}
+\inferrule*[Left={$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R}
 \\
 \inferrule*[left=$\Rightarrow$Élim]{
-\inferrule*[left=\llap{Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P}
+\inferrule*[Left={Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P}
 \\\Gamma\vdash M}{\Gamma,M\Rightarrow P\vdash P}
 }{\Gamma,M\Rightarrow P\vdash R}$
 \end{tabular}
@@ -2946,16 +2946,16 @@ branches de la coupure n'opère pas sur la formule coupée : on fait
 \begin{center}
 \scalebox{0.65}{%
 $\inferrule*[left={\color{purple}Cut}]{
-\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
+\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
 \\
-\inferrule*[right=\rlap{?}]{\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}}{\Gamma,P_1\land P_2\vdash Q}
+\inferrule*[Right={?}]{\mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}}{\Gamma,P_1\land P_2\vdash Q}
 }{\Gamma\vdash Q}$
 }
 ~devient~
 \scalebox{0.65}{%
-$\inferrule*[right=\rlap{?}]{
-\inferrule*[left=\llap{\color{purple}Cut}]{
-\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
+$\inferrule*[Right={?}]{
+\inferrule*[Left={\color{purple}Cut}]{
+\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
 \\
 \mpdotsabove{\Gamma',P_1\land P_2\vdash Q'}
 }{\Gamma,\Gamma'\vdash Q'}
@@ -2996,9 +2996,9 @@ de complexité de la formule coupée diminue :
 \begin{center}
 \scalebox{0.8}{%
 $\inferrule*[left={\color{purple}Cut}]{
-\inferrule*[left=\llap{$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
+\inferrule*[Left={$\land$R}]{\mpdotsabove{\Gamma \vdash P_1}\\\mpdotsabove{\Gamma \vdash P_2}}{\Gamma \vdash P_1\land P_2}
 \\
-\inferrule*[right=\rlap{$\land$L$_1$}]{\mpdotsabove{\Gamma,P_1\vdash Q}}{\Gamma,P_1\land P_2\vdash Q}
+\inferrule*[Right={$\land$L$_1$}]{\mpdotsabove{\Gamma,P_1\vdash Q}}{\Gamma,P_1\land P_2\vdash Q}
 }{\Gamma\vdash Q}$
 }
 ~devient~
@@ -3014,9 +3014,9 @@ $\inferrule*[left={\color{purple}Cut}]{
 \begin{center}
 \scalebox{0.7}{%
 $\inferrule*[left={\color{purple}Cut}]{
-\inferrule*[left=\llap{$\Rightarrow$R}]{\mpdotsabove{\Gamma, M\vdash P}}{\Gamma \vdash M\Rightarrow P}
+\inferrule*[Left={$\Rightarrow$R}]{\mpdotsabove{\Gamma, M\vdash P}}{\Gamma \vdash M\Rightarrow P}
 \\
-\inferrule*[right=\rlap{$\Rightarrow$L}]{\mpdotsabove{\Gamma \vdash M}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\Rightarrow P\vdash Q}
+\inferrule*[Right={$\Rightarrow$L}]{\mpdotsabove{\Gamma \vdash M}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\Rightarrow P\vdash Q}
 }{\Gamma\vdash Q}$
 }
 ~devient~
@@ -3024,7 +3024,7 @@ $\inferrule*[left={\color{purple}Cut}]{
 $\inferrule*[left={\color{purple}Cut}]{
 \mpdotsabove{\Gamma \vdash M}
 \\
-\inferrule*[right=\rlap{{\color{purple}Cut}}]{\mpdotsabove{\Gamma,M \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\vdash Q}
+\inferrule*[Right={{\color{purple}Cut}}]{\mpdotsabove{\Gamma,M \vdash P}\\\mpdotsabove{\Gamma,P\vdash Q}}{\Gamma,M\vdash Q}
 }{\Gamma\vdash Q}$
 }
 \end{center}