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

  \begin{exampleblock}{$\myall{x}{(P(x) \to \neg P(x))} \;\vdash\; \myall{x}{ \neg P(x)}$}
  \mpause[1]{
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myall{x}{ (P(x) \to \neg P(x)) }$}{premise};
      \namedproofbox{$x_0$}{
        \proofbox{
          \proofstep{$P(x_0)$}{assumption};
          \proofstep{$P(x_0) \to \neg P(x_0)$}{$\forall e\; 1$};
          \proofstep{$\neg P(x_0)$}{$\to_e\; 2,3$};
          \proofstep{$\bot$}{$\neg e\; 2,4$};
        }
        \proofstep{$\neg P(x_0)$}{$\neg i\;$ 2--5};
      }
      \proofstep{$\myall{x}{\neg P(x)}$}{$\forall i\; $2--6};
    }
  \end{tikzpicture}
  }
  \end{exampleblock}

  \begin{exampleblock}{}
    {\scriptsize%
    \begin{verbatim}Theorem ex4 : all x, (P(x) -> ~P(x)) -> all x, ~P(x).
\end{verbatim}
\pause\pause\vspace{-4.75ex}

\begin{verbatim}Proof.
imp_i H. all_i x0. neg_i HPx0.
insert Himp (P(x0) -> ~P(x0)). f_all_e H.
insert HnPx0 (~P(x0)).
f_imp_e Himp HPx0.
f_neg_e HnPx0 HPx0.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}