\begin{frame}
  \small
  
  \begin{definitions}
  \begin{itemize}
  \item
  \makebox[8mm][l]{\alert<1>{$\subsumes$}} \alert<1>{subsumption}
  \\[.5ex]
  \makebox[8mm][l]{$s \subsumes t$}
  $~\iff~\exists \sigma\colon s\sigma = t$ \qquad
  \onslide<2->``$s$ \alert<.>{subsumes} $t$'' \quad
  ``$t$ is \alert<.>{instance} of $s$''
  \item<3->
  \makebox[8mm][l]{\alert<3>{$\prsubsumes$}} \alert<3>{proper} subsumption
  \\[.5ex]
  \makebox[8mm][l]{$s \prsubsumes t$}
  $~\iff~s \subsumes t ~\wedge~ \neg (t \subsumes s)$
  \end{itemize}
  \end{definitions}
  \pause\pause\pause
  \bigskip
  
  \begin{example}
  \smallskip
  $\GREEN{x+y} \subsumes \GREEN{\m{s}(y)+\m{s}(0)}$
  \qquad 
  $\GREEN{\m{s}(x)+y} \not\subsumes \GREEN{x+\m{s}(0)}$
  \qquad 
  $\GREEN{\m{s}(x)+y} \subsumes \GREEN{\m{s}(x)+x}$
  \end{example}
  \pause
  \bigskip
  
  \begin{lemma}
  \smallskip
  $\prinstance$ is well-founded order on terms
  \smallskip
  \end{lemma}
\end{frame}