51/77
\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}