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