\begin{frame}[fragile] \frametitle{Previous Example in ProofWeb} \begin{exampleblock}{} {\small% \begin{verbatim}Theorem ex10 : all x, (P(x) \/ Q(x)) -> (all x, P(x)) \/ (exi x, Q(x)). \end{verbatim} \pause\vspace{-4ex} \begin{verbatim}Proof. imp_i H. insert Hor ((exi x, Q x) \/ ~(exi x, Q x)). LEM. f_dis_e Hor He Hne. f_dis_i2 He. dis_i1. all_i x0. insert Hx0 (P(x0) \/ Q(x0)). f_all_e H. f_dis_e Hx0 Px0 Qx0. ass Px0. insert He (exi x, Q x). f_exi_i Qx0. fls_e. f_neg_e Hne He. Qed.\end{verbatim}% } \end{exampleblock} \end{frame}