15/19
\begin{frame}[fragile]
  \frametitle{Examples}
  
  \vspace{-1ex}
  \begin{exampleblock}{Example: $(a \to b) \wedge (b \to a) \;\;\vdash\;\; (a \wedge b) \vee (\neg a \wedge \neg b)$}
  \vspace{-1ex}
  \medskip{\small
  \begin{verbatim}
Theorem ex6 : (A -> B) -> (B -> A) 
              -> ((A /\ B) \/ (~A /\ ~B)).\end{verbatim}
  \pause

  \begin{verbatim}
  Proof.
  imp_i HAB. imp_i HBA.
  dis_e (A \/ ~A) HA HnA.
  LEM.
  dis_i1.
  con_i.
  ass HA.
  imp_e A.
  ass HAB. ass HA.
  dis_i2.
  con_i.
  ass HnA.
  MT (A).
  ass HBA. ass HnA.
  Qed.\end{verbatim}
  }
  \end{exampleblock}  
\end{frame}