diff --git a/RapportPresentation/ex-presentation.tex b/RapportPresentation/ex-presentation.tex
index 5170b3a..83ef093 100644
--- a/RapportPresentation/ex-presentation.tex
+++ b/RapportPresentation/ex-presentation.tex
@@ -4,7 +4,9 @@
 \usepackage{listings}
 \usepackage{syntax}
 \usepackage[utf8]{inputenc}
+\usepackage{xcolor}
 \newcommand{\Hquad}{\hspace{0.2em}}
+\newcommand{\red}[1]{\textbf{\color{red}#1}}
 
 \lstset{
  language=caml,
@@ -60,8 +62,24 @@
   Preuve $\Leftrightarrow$ programme du $\lambda$-calcul simplement typé
 \end{frame}
 
-\begin{frame}{lambda-calcul}
-  la grammaire
+\begin{frame}{$lambda$-calcul}
+  les types sont donnés par
+
+  \lstinline{<A, B> ::= X}
+
+	\lstinline{| A -> B}
+
+	\lstinline{| A /\\ B}
+
+	\lstinline{| A \\/ B}
+
+	\lstinline{| false}
+
+  On peut avoir les $\lambda$-termes suivants:
+
+  \lstinline{fun (x:A) => x}
+
+  \lstinline{fun (x:A) => exf(x:B)}
 \end{frame}
 
 %! liste des tactiques
@@ -106,10 +124,10 @@
   \frametitle{Prouvons $(A \rightarrow B \rightarrow C) \rightarrow A \rightarrow B \rightarrow C$}
 
   Preuve: %rajouter les types
-  \only<1>{$$?$$}
-  \only<2>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow ?$$}
-  \only<3>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad ? \Hquad ?)$$}
-  \only<4>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad x_1 \Hquad ?)$$}
+  \only<1>{$$\red{?}$$}
+  \only<2>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow \red{?}$$}
+  \only<3>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad \red{?} \Hquad ?)$$}
+  \only<4>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad x_1 \Hquad \red{?})$$}
   \only<5-6>{$$fun \Hquad (x_0:(A \rightarrow (B \rightarrow C))) \Rightarrow fun \Hquad (x_1:A) \Rightarrow fun \Hquad (x_2:B) \Rightarrow (x_0 \Hquad x_1 \Hquad x_2)$$}
 
   Interface:
@@ -146,8 +164,12 @@
 \end{frame}
 
 
-\begin{frame}
-  \frametitle{Fiabilité}
+\begin{frame}{Fiabilité}
+  \begin{itemize}
+    \item Comment être sûrs de nos preuves
+    \pause
+    \item Envoyer nos termes de preuves à \textbf{\color{blue}{Coq}}.
+  \end{itemize}
 \end{frame}
 
 \end{document}