\begin{frame}[fragile]
  \frametitle{Examples}
  
  \begin{exampleblock}{Example: $p \vee q,\;\; \neg p \;\;\vdash\;\; q$}
  \pause\medskip{\small
  \begin{verbatim}
Theorem ex1 : (A \/ B) -> ~A -> B.\end{verbatim}
  \pause
  \begin{verbatim}
  Proof.
  imp_i H.
  imp_i HnA.
  dis_e (A \/ B) HA HB.
  ass H.
  fls_e.
  neg_e (A).
  ass HnA.
  ass HA.
  ass HB.
  Qed.\end{verbatim}
  \smallskip}
  \end{exampleblock}  
\end{frame}