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

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

  \begin{exampleblock}{}
    {\scriptsize%
    \begin{verbatim}Theorem ex9 : exi x, all y, R(x,y) -> all y, exi x, R(x,y).
\end{verbatim}
\pause\pause\vspace{-4.5ex}

\begin{verbatim}Proof.
imp_i H. all_i y0.
f_exi_e H x0 Hx0.
insert Rx0y0 (R(x0,y0)).
f_all_e Hx0.
f_exi_i Rx0y0.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}