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