\begin{frame}<1-3>[label=development example]
  \small
  
  \begin{definition}
  \smallskip
  A \alert<1>{development} of set of redex positions $Q$ in term $t$ is a rewrite
  sequence starting \\ from $t$ in which all contracted redex positions
  descend from positions in $Q$.
  \end{definition}
  
  \bigskip
  
  \begin{example}
  \smallskip
  \begin{itemize}
  \item
  rewrite rules
  \vspace{-1ex}
  \GREEN{\begin{xalignat*}{2}
  \m{0} + y & \to y &
  \m{0} \times y &\to \m{0} \\
  \m{s}(x) + y &\to \m{s}(x + y) &
  \m{s}(x) \times y &\to (x \times y) + y 
  \end{xalignat*}}
  \vspace{-3ex}
  \item
  rewrite sequences
  \vspace{-1ex}
  \GREEN{\begin{alignat*}{2}
  \underline{\m{s}(\m{0}) \alert{\times} (\m{0} \alert{\times} \m{0})}
  &\to (\m{0} \times \underline{(\m{0} \alert{\times} \m{0})}) + (\m{0} \alert{\times} \m{0})
  \to (\m{0} \times \m{0}) + (\m{0} \alert{\times} \m{0})
  &\qquad&
  \only{\alt<5>{\huil}{\lach}}
  \only{\lach}
  \\
  \onslide<2->{\underline{\m{s}(\m{0}) \alert{\times} (\m{0} \alert{\times} \m{0})}}
  &\onslide<2->{\to
  \underline{(\m{0} \times (\m{0} \alert{\times} \m{0})}) + (\m{0} \alert{\times} \m{0})
  \to \m{0} + (\m{0} \alert{\times} \m{0})}
  && \onslide<2->{\huil}
  \\
  \onslide<3->{\m{s}(\m{0}) \alert{\times} \underline{(\m{0} \alert{\times} \m{0})}}
  &\onslide<3->{\to \underline{\m{s}(\m{0}) \alert{\times} \m{0}}
  \to (\m{0} \times \m{0}) + \m{0}}
  && \onslide<3->{\lach}
  \end{alignat*}}
  \vspace{-3ex}
  \end{itemize}
  \end{example}
\end{frame}