\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}