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