\begin{frame}[fragile] \frametitle{Examples} \begin{exampleblock}{$\vdash\; \myall{x}{(P(x) \to P(x))}$} \mpause[1]{ \begin{tikzpicture} \naturaldeduction{ \namedproofbox{$x_0$}{ \proofbox{ \proofstep{$P(x_0)$}{assumption}; } \proofstep{$P(x_0) \to P(x_0)$}{$\to i\;$ 2--2}; } \proofstep{$\myall{x}{(P(x) \to P(x))}$}{$\forall i\;$ 1--3}; } \end{tikzpicture} } \end{exampleblock} \begin{exampleblock}{} {\small% \begin{verbatim}Theorem ex2 : all x, ( P(x) -> P(x) ). \end{verbatim} \pause\pause\vspace{-4ex} \begin{verbatim}Proof. all_i x0. imp_i H. ass H. Qed.\end{verbatim}% } \end{exampleblock} \end{frame}