\begin{frame}[fragile]
  \frametitle{Examples}
  
  \begin{exampleblock}{Example: $\vdash\;\; ((p \to q) \to p) \to p$}
  \medskip{\small
  \begin{verbatim}
Theorem ex8 : ((A -> B) -> A) -> A.\end{verbatim}
  \pause
  \begin{verbatim}
  Proof.
  imp_i H.
  dis_e (A \/ ~A) HA HnA.
  LEM.
  ass HA.
  imp_e (A -> B).
  ass H.
  imp_i HA.
  fls_e.
  f_neg_e HnA HA.
  Qed.\end{verbatim}
  \smallskip}
  \end{exampleblock}  
\end{frame}