summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--exercices-inf110.tex5
1 files changed, 4 insertions, 1 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index a8bf66a..2f00df0 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2384,7 +2384,10 @@ La revoici écrite dans le style « drapeau » :
\end{footnotesize}
\egroup
-La voici réécrite en forme d'arbre de preuve :
+La voici réécrite en forme d'arbre de preuve (en omettant certaines
+hypothèses superflues à gauche du symbole ‘$\vdash$’, ou, ce qui
+revient au même, en faisant un usage tacite de la règle
+d'affaiblissement) :
\begin{tiny}
\[
\inferrule*[left={$\Rightarrow$Int}]{