Fix a number of typos / thinkos / notational blunders in an exercise.

1 files changed, 4 insertions, 4 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 43ca6c6..6b1f15b 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1945,8 +1945,8 @@ En Coq, cette preuve s'écrit :
 {\tt
 Parameter A B C : Prop.\\
 Theorem thm : A\textbackslash /B -> ((A->B)->B) /\textbackslash\ ((B->A)->A).\\
-Proof.  intro H.  destruct H.  split.  intro H0.  apply H0.  exact H.
-intro H0.  exact H.  split.  intro H0. exact H.  intro H0. apply H0.
+Proof.  intro H.  destruct H.  split.  intro H1.  apply H1.  exact H.
+intro H2.  exact H.  split.  intro H1.  exact H.  intro H2.  apply H2.
 exact H.  Qed.
 \par}
 
@@ -1960,13 +1960,13 @@ preuve en question :
 \lambda(h_2:B\Rightarrow A).\,h_0\rangle,\\
 &\iota_2 h_0
 \mapsto \langle \lambda(h_1:A\Rightarrow B).\,h_0,\;
-\lambda(h_2:B\Rightarrow A).\,h_1 h_0\rangle)
+\lambda(h_2:B\Rightarrow A).\,h_2 h_0\rangle)
 \end{aligned}
 \]
 (ou en syntaxe Coq : \texttt{(fun H : A \textbackslash/ B =>
  match H with
    or\_introl H0 => conj (fun H1 : A -> B => H1 H0) (fun H2 : B -> A => H0)
- | or\_intror H0 => conj (fun H2 : A -> B => H0) (fun H1 : B -> A => H1 H0)
+ | or\_intror H0 => conj (fun H1 : A -> B => H0) (fun H2 : B -> A => H2 H0)
  end)})
 \end{corrige}