\begin{frame}
  
  \begin{definitions}
  \begin{itemize}[<+->]
  \item
  \makebox[8mm][l]{\alert<1>{$\doteq$}} \alert<1>{literal similarity}
  \\[.5ex]
  \makebox[8mm][l]{$s \doteq t$}
  $~\iff~s \subsumes t ~\wedge~ t \subsumes s$
  \item
  \alert<2>{variable substitution} is substitution from $\VV$ to $\VV$
  \item
  \alert<3>{renaming} is bijective variable substitution
  \item
  terms $s$ and $t$ are \alert<4>{variants} if $s = t\sigma$ for some
  renaming $\sigma$
  \smallskip
  \end{itemize}
  \end{definitions}
  
  \bigskip
  
  \begin{lemma}<5->
  \smallskip
  terms $s$ and $t$ are variants \quad$\iff$\quad $s \doteq t$
  \smallskip
  \end{lemma}
  
  \bigskip
  
  \begin{example}<6->
  \smallskip
  $\GREEN{\m{s}(x)+\m{s}(y+\m{0})} \doteq \GREEN{\m{s}(y)+\m{s}(z+\m{0})}$
  \qquad \onslide<7->
  $\GREEN{\m{s}(x)+\m{s}(y+\m{0})} \not\doteq
  \GREEN{\m{s}(x)+\m{s}(x+\m{0})}$
  \end{example}
\end{frame}