\begin{frame}
  \frametitle{Natural Deduction: Quantifiers}
  
  \vspace{-1ex}
  \begin{goal}{Elimination of Existential Quantification}
    \vspace{-1ex}
    \begin{align*}
      \infer[\rulename{\exists_e}]
      {\psi}
      {
        \myex{x}{\phi} &&
        \framebox{\parbox{1.8cm}{\hint{$x_0$}\\\centerline{$\phi[x_0/x]$}\\\centerline{$\vdots$}\\\centerline{$\psi$}}}
      }
    \end{align*}\vspace{-3.5ex}
    
    \emph{Condition}: $x_0$ nowhere outside the box (in particular not in $\psi$).
  \end{goal}
  \pause

  \begin{exampleblock}{$\myex{x}{(P(x) \wedge Q(x))} \;\vdash\; \myex{x}{P(x)}$}
  \begin{tikzpicture}
  \naturaldeduction{
    \mpause[1]{
      \proofstep{$\myex{x}{(P(x) \wedge Q(x))}$}{premise};
    }
    \mpause{
      \namedproofbox{$x_0$}{
        \mpause{
        \proofstep{$P(x_0) \wedge Q(x_0)$}{assumption};
        }
        \mpause{
        \proofstep{$P(x_0)$}{$\wedge_e$ 2};
        }
        \mpause{
        \proofstep{$\myex{x}{P(x)}$}{$\exists_i$ 3};
        }
      }
    }
    \mpause{
    \proofstep{$\myex{x}{P(x)}$}{$\exists_e$ 1,2--4};
    }
  }
  \end{tikzpicture}\vspace{-1ex}
  \end{exampleblock}
\end{frame}