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

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

  \begin{exampleblock}{}
    {\small%
    \begin{verbatim}Theorem ex7 : exi x, R(x,x) -> exi x, exi y, R(x,y).
\end{verbatim}
\pause\pause\vspace{-4ex}

\begin{verbatim}Proof.
imp_i H.
f_exi_e H z Hz.
insert H2 (exi y, R(z,y)).
f_exi_i Hz.
f_exi_i H2.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}