\begin{frame}[fragile]
  \frametitle{Examples (from a final exam)} 

  \begin{exampleblock}{$\myex{x}{P(x) \to Q(c)} \;\vdash\; \myall{x}{(P(x) \to Q(c))}$}
  \mpause[1]{
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myex{x}{P(x) \to Q(c)}$}{premise};
      \namedproofbox{$y$}{
        \proofbox{
          \proofstep{$P(y)$}{assumption};
          \proofstep{$\myex{x}{P(x)}$}{$\exists i\; 2$};
          \proofstep{$Q(c)$}{$\to e\; 1,3$};
        }
        \proofstep{$P(y) \to Q(c)$}{$\to i\;$ 2--4};
      }
      \proofstep{$\myall{x}{(P(x) \to Q(c))}$}{$\forall i\; $1--5};
    }
  \end{tikzpicture}
  }
  \end{exampleblock}

  \begin{exampleblock}{}
    {\scriptsize%
\begin{verbatim}Theorem ex3 : (exi x, P(x) -> Q(c)) -> all x, (P(x) -> Q(c)).
\end{verbatim}
\pause\pause\vspace{-4ex}

\begin{verbatim}Proof.
imp_i H.
all_i x0.
imp_i Px0.
insert Hexi (exi x, P x).
f_exi_i Px0.
f_imp_e H Hexi.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}