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

  \begin{exampleblock}{$\myall{x}{(A(x) \wedge  B(x))} \;\vdash\; \myall{x}{B(x)}$}
  \mpause[1]{
  \begin{tikzpicture}
    \naturaldeduction{
      \proofstep{$\myall{x}{(A(x) \wedge B(x))}$}{premise};
    \namedproofbox{$x_0$}{
        \proofstep{$A(x_0) \wedge B(x_0)$}{$\forall e\;$ 1};
        \proofstep{$B(x_0)$}{$\wedge e\;$ 2};
    }
    \proofstep{$\myall{x}{B(x)}$}{$\forall i\;$ 1--3};
    }
  \end{tikzpicture}
  }
  \end{exampleblock}

  \begin{exampleblock}{}
    {\small%
\begin{verbatim}Theorem ex1 : all x, (A(x) /\ B(x)) -> all x, B(x).
\end{verbatim}
\pause\pause\vspace{-4ex}

\begin{verbatim}Proof.
imp_i H.
all_i x0.
insert HAB (A(x0) /\ B(x0)).
f_all_e H.
f_con_e2 HAB.
Qed.\end{verbatim}%
}
  \end{exampleblock}
\end{frame}