\begin{frame}
  \small
  
  \begin{definition}
  \smallskip
  \alert<1>{composition} of substitutions $\sigma$ and $\tau$:
  \[
  \alert<1>{\sigma\tau} = \{ x \mapsto \sigma(x)\tau \mid x \in \VV \}
  \]
  \end{definition}
  
  \medskip
  
  \begin{example}<2->
  \smallskip
  $\sigma = \{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},
  \GREEN{y} \mapsto \GREEN{x + \m{s(0)}} \}$
  \quad
  $\tau = \{ \GREEN{x} \mapsto \GREEN{\m{s(0)}},
  \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(y))} \}$
  \begin{itemize}
  \item<3->
  $\sigma\tau = \{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},
  \GREEN{y} \mapsto \GREEN{\m{s(0) + s(0)}},
  \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(y))} \}$
  \item<4->
  $\tau\sigma = \{ \GREEN{x} \mapsto \GREEN{\m{s(0)}},
  \GREEN{y} \mapsto \GREEN{x + \m{s(0)}},
  \GREEN{z} \mapsto \GREEN{\m{s}(\m{s}(x + \m{s(0)}} \}$
  \end{itemize}
  \end{example}
  
  \medskip
  
  \begin{lemma}<5->
  \smallskip
  $(\rho\sigma)\tau = \rho(\sigma\tau)$
  for all substitutions $\rho$, $\sigma$, $\tau$
  \end{lemma}
\end{frame}