\begin{frame}
  \frametitle{Natural Deduction: Quantifiers}
  
  \begin{goal}{Elimination of Universal Quantification}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\forall_e}]
      {\phi\;[t/x]}
      {\myall{x}{\phi}}
    \end{align*}
    \pause
    \emph{Condition} for application of this rule: $t$ free for $x$ in $\phi$.
  \end{goal}
  \pause\medskip

  \begin{exampleblock}{$\myall{x}{P(x)} \;\vdash\; \myex{x}{P(x)}$}
  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
    \proofstep{$\myall{x}{P(x)}$}{premise};
    }
    \mpause{
    \proofstep{$P(z)$}{$\forall_e$ 1};
    }
    \mpause{
    \proofstep{$\myex{x}{P(x)}$}{$\exists_i$ 2};
    }
  }
  \end{tikzpicture}
  \\
  \mpause[2]{\hint{For line 2\mpause{, 3}:\quad $P(z) = P(x) [z/x]$}}
  \end{exampleblock}
\end{frame}