\begin{frame}
  \frametitle{Natural Deduction: Quantifiers}
  
  \begin{goal}{Introduction of Universal Quantification}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\forall_i}]
      {\myall{x}{\phi}}
      {
        \framebox{\parbox{1.8cm}{\hint{$x_0$}\\\centerline{$\vdots$}\\\centerline{$\phi\;[x_0/x]$}}}
      }
    \end{align*}
    \emph{Condition} for application of this rule: `$x_0$ is arbitrary'.\\
    That is: $x_0$ occurs only inside the box (in particular not in $\phi$)
  \end{goal}
  \pause\medskip

  \begin{exampleblock}{$\vdash\; \myall{x}{(P(x) \to P(x))}$}
  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
      \namedproofbox{$x_0$}{
        \mpause{
          \proofbox{
            \mpause{
            \proofstep{$P(x_0)$}{assumption};
            }
          }
        }
        \mpause{
        \proofstep{$P(x_0) \to P(x_0)$}{$\to_i$ 1--1};
        }
      }
    }
    \mpause{
    \proofstep{$\myall{x}{(P(x)\to P(x))}$}{$\forall_i$ 1--2};
    }
  }
  \end{tikzpicture}
  \end{exampleblock}
\end{frame}