\begin{frame}
  \small
  
  \begin{definition}[Unification Rules]
  \begin{itemize}[<+->]
  \item[\alert<1>{$\mathsf{d}$}]~
  \alert<1>{decomposition}\\
  \[
  \frac{E_1,\:f(\seq{s}) \approx f(\seq{t}),\:E_2}
  {E_1,\:s_1 \approx t_1,\:\dots,\:s_n \approx t_n,\:E_2}
  \]
  \item[\alert<2>{$\mathsf{t}$}]~
  \makebox[45mm][l]{\alert<2>{removal of trivial equations}} ($x \in \VV$) \\
  \[
  \frac{E_1,\:x \approx x,\:E_2}{E_1,\:E_2}
  \]
  \item[\alert<3>{$\mathsf{v}$}]~
  \makebox[45mm][l]{\alert<.>{variable elimination}} ($x \in \VV$) \\
  \[
  \frac{E_1,\:x \approx t,\:E_2}{(E_1,\:E_2)\alert<.>{\sigma}}
  \quad \text{and} \quad
  \frac{E_1,\:t \approx x,\:E_2}{(E_1,\:E_2)\alert<.>{\sigma}}
  \]
  ~ if $\underbrace{x \notin \Var(t)}_%
  {\makebox[0mm][c]{\alert<3>{occurs check}}}$ and
  $\alert<3>{\sigma = \{ x \mapsto t \}}$
  \smallskip
  \end{itemize}
  \end{definition}
\end{frame}