6/19
\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}