Exercise had already been explained during course. Change it.

1 files changed, 9 insertions, 10 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 740aaa1..0e3c269 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -193,21 +193,20 @@ pour terminer la démonstration).
 Donner une démonstration en calcul propositionnel intuitionniste de la
 formule suivante :
 \[
-(A\Rightarrow B\Rightarrow C) \Rightarrow (B\Rightarrow A\Rightarrow C)
+A \Rightarrow (A\Rightarrow B) \Rightarrow B
 \]
 On donnera la démonstration sous la forme qu'on préfère (arbre de
-preuve, style drapeau, ou même simplement précisément écrite en
-français), puis on donnera aussi un $\lambda$-terme de preuve.  On
-décrira ensuite brièvement ce que fait ce terme vu en tant que
-programme (i.e., le comportement du programme associé à la preuve par
-la correspondance de Curry-Howard).
+preuve ou style drapeau), puis on donnera aussi un $\lambda$-terme de
+preuve.  On décrira ensuite brièvement ce que fait ce terme vu en tant
+que programme (i.e., le comportement du programme associé à la preuve
+par la correspondance de Curry-Howard).
 
 \begin{corrige}
 \textcolor{red}{Corrigé de cet exercice à écrire.  Ce qui suit est un
-  résumé.}  Le $\lambda$-terme est $\lambda(f:A\Rightarrow
-B\Rightarrow C).\, \lambda(y:B).\, \lambda(x:A).\, f x y$ et il
-échange les deux arguments d'une fonction de deux variables donnée
-sous forme curryfiée.
+  résumé.}  Le $\lambda$-terme est $\lambda(x:A).\,
+\lambda(k:A\Rightarrow B).\, k x$, et le programme transforme $x$ en
+la fonction qui applique une fonction $k$ à $x$, ou, ce qui revient au
+même, il prend successivement $x$ et $k$ et applique $k$ à $x$.
 \end{corrige}