\begin{frame}[fragile]
  \frametitle{Examples}

  \begin{exampleblock}{$\myex{x}{(P(x) \wedge Q(x))} \;\vdash\; \myex{x}{P(x)}$}
  \mpause[1]{
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myex{x}{(P(x) \wedge Q(x))}$}{premise};
    \namedproofbox{$x_0$}{
        \proofstep{$P(x_0) \wedge Q(x_0)$  }{assumption};   
        \proofstep{$P(x_0)$}{$\wedge_e\;$ 2};
        \proofstep{$\myex{x}{P(x)}$}{$\exists_i\;$ 3};
    }
    \proofstep{$\myex{x}{P(x)}$}{$\exists_e\;$ 1, 2--4};
    }
  \end{tikzpicture}
  }
  \end{exampleblock}

  \begin{exampleblock}{}
    {\small%
    \begin{verbatim}Theorem ex6 : exi x, (P(x) /\ Q(x)) -> exi x, P(x).
\end{verbatim}
\pause\pause\vspace{-4ex}

\begin{verbatim}Proof.
imp_i H.
f_exi_e H y Hy.
insert HPy (P(y)).
f_con_e1 Hy.
f_exi_i HPy.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}