\begin{frame}[fragile] \frametitle{Examples} \begin{exampleblock}{Example: $a \vee b,\;\; a \to c,\;\; \neg d \to \neg b \;\;\vdash\;\; c \vee d$} \medskip{\small \begin{verbatim} Theorem ex5 : (A \/ B) -> (A -> C) -> (~D -> ~B) -> (C \/ D).\end{verbatim} \pause \begin{verbatim} Proof. imp_i HAoB. imp_i HAC. imp_i HDB. f_dis_e HAoB HA HB. dis_i1. imp_e A. ass HAC. ass HA. dis_i2. PBC HD. neg_e (B). imp_e (~D). ass HDB. ass HD. ass HB. Qed.\end{verbatim} \smallskip} \end{exampleblock} \end{frame}