summaryrefslogtreecommitdiffstats
path: root/transp-inf110-03-quantif.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-03-quantif.tex')
-rw-r--r--transp-inf110-03-quantif.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index e0e44b9..08001c0 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -928,8 +928,8 @@ Présentation avec les seules conclusions :
\step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y$}
\step{exbare}{\exists x'.B(x',y')}{$\exists$Int sur $x$ et \ref{bare}}
\conclude{extrude}{\exists x'.B(x',y')}{$\exists$Elim sur \ref{mainhyp} de \ref{exhyp} dans \ref{exbare}}
-\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Intro de \ref{vary} dans \ref{extrude}}
-\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Intro de \ref{mainhyp} dans \ref{mainconc}}
+\conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Int de \ref{vary} dans \ref{extrude}}
+\conclude{}{(\exists x.\forall y.B(x,y))\Rightarrow(\forall y'.\exists x'.B(x',y'))}{$\Rightarrow$Int de \ref{mainhyp} dans \ref{mainconc}}
\end{flagderiv}
\par}