diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 02917f0..770627e 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -445,7 +445,7 @@ donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle {\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $s$ mais pas dans $\Gamma$ ni $Q$.)} \[ -\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q} +\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q} \] \medskip @@ -494,7 +494,7 @@ $\forall$ \\\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}$} -&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$} +&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$} \\ \end{tabular} |