\begin{frame}[fragile] \frametitle{Examples} \begin{exampleblock}{Example: $p \to (q \to r) \;\;\vdash\;\; q \to (p \to r)$} \medskip{\small \begin{verbatim} Theorem ex2 : (A -> (B -> C)) -> (B -> (A -> C)).\end{verbatim} \pause \begin{verbatim} Proof. imp_i H. imp_i HB. imp_i HA. imp_e B. imp_e A. ass H. ass HA. ass HB. Qed.\end{verbatim} \smallskip} \end{exampleblock} \end{frame}