\begin{frame}
  \small
  
  \begin{definition}[Unification Problem]
  \smallskip
  \begin{tabular}{ll@{\qquad\qquad}ll}
  instance: & terms $s$, $t$ \\[.5ex]
  question: & $\exists$
  $\underbrace{\mathstrut\text{substitution $\sigma$}}_%
  {\makebox[0mm][c]{\alert<1>{unifier}}}\colon ~ s\sigma = t\sigma$ ?
  \end{tabular}
  \end{definition}
  
  \smallskip
  
  \begin{definition}<2->
  \smallskip
  substitution $\sigma$ is \alert<2>{at least as general} as $\tau$
  ($\alert<2>{\sigma \subsumes \tau}$) if
  $\exists$ substitution $\rho\colon \sigma\rho = \tau$
  \smallskip
  \end{definition}
  
  \smallskip
  
  \begin{lemma}<3->
  \smallskip
  $\prinstance$ is well-founded order on substitutions (with a finite domain)
  \smallskip
  \end{lemma}
  
  \smallskip
  
  \begin{definition}<4->
  \smallskip
  \alert<4>{most general} unifier (\alert<4>{mgu}) is at least as general as
  any other unifier
  \end{definition}
\end{frame}