60/77
\begin{frame}[fragile]
  \frametitle{Examples}

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

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

\begin{verbatim}Proof.
imp_i H.
all_i x0.
PBC HnAx0.
insert H2 (exi x, ~A(x)).
f_exi_i HnAx0.
f_neg_e H H2.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}