\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}