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

  \begin{exampleblock}{$\myall{x}{A(x)} \;\vdash\; \neg \myex{x}{\neg A(x)}$}
  \mpause[1]{
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myall{x}{A(x)}$}{premise};
      \proofbox{
        \proofstep{$\myex{x}{\neg A(x)}$}{assumption};  
        \namedproofbox{$x_0$}{
          \proofstep{$\neg A(x_0)$}{assumption};
          \proofstep{$A(x_0)$}{$\forall_e\; 1$};
          \proofstep{$\bot$}{$\neg_e\; 3,4$};
        }
      \proofstep{$\bot$}{$\exists_e\;$ 2, 3--5};
    }
    \proofstep{$\neg \myex{x}{\neg A(x)}$}{$\neg_i\;$ 2--6};
    }
  \end{tikzpicture}
  }
  \end{exampleblock}

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

\begin{verbatim}Proof.
imp_i H.
neg_i H2.
f_exi_e H2 y Hny.
insert Hy (A(y)). f_all_e H.
f_neg_e Hny Hy.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}