50/73
\begin{frame}
  \vspace{-1ex}
  {\renewcommand{\arraystretch}{0.7}
  \begin{example}
  \begin{minipage}{65mm}
  \[
  \begin{array}[t]{c}
  \GREEN{x\alert<2,3>{+}(\m{0}+\m{s}(y)) \approx
  \m{s}(z)\alert<2,3>{+}(\m{0}+x)}
  \\[1ex]
  \onslide<3->\derive{d}{}
  \\[1ex]
  \GREEN{\alert<4>{x \approx \m{s}(z)},~\m{0}+\m{s}(y) \approx \m{0}+x}
  \\[1ex]
  \onslide<4->\derive{v}{\GREEN{\alert<4,10>{x \mapsto \m{s}(z)}}}
  \\[1ex]
  \GREEN{\m{0}\alert<5>{+}\m{s}(y) \approx \m{0}\alert<5>{+}\m{s}(z)}
  \\[1ex]
  \onslide<5->\derive{d}{}
  \\[1ex]
  \GREEN{\alert<6>{\m{0}} \approx \alert<6>{\m{0}},~\m{s}(y) \approx
  \m{s}(z)}
  \\[1ex]
  \onslide<6->\derive{d}{}
  \\[1ex]
  \GREEN{\alert<7>{\m{s}}(y) \approx \alert<7>{\m{s}}(z)}
  \\[1ex]
  \onslide<7->\derive{d}{}
  \\[1ex]
  \GREEN{\alert<8>{y \approx z}}
  \\[1ex]
  \onslide<8->\derive{v}{\GREEN{\alert<8,10>{y \mapsto z}}}
  \\[1ex]
%   \GREEN{\alert<9>{z \approx z}}
%   \\[1ex]
%   \onslide<9->\derive{t}{}
%   \\[1ex]
  \onslide<8->\GREEN{\alert<9>{\Box}}
  \end{array}
  \]
  \end{minipage}
  \onslide<10->
  \begin{minipage}{40mm}
  mgu \quad
  \GREEN{$\{ x \mapsto \m{s}(z), y \mapsto z \}$}
  \end{minipage}
  \end{example}
  }
\end{frame}