\begin{frame}
  \small
  
  \begin{example}
  \smallskip
  ES $\EE$
  \[
  \GREEN{\begin{array}{r@{~}c@{~}l}
  \m{0}+y & \approx & y \\[.5ex]
  \m{s}(x)+y & \approx & \m{s}(x+y) 
  \end{array}}
  \]
  
  \medskip
  
  $\EE \vdash \GREEN{\m{s(s(0)}+\m{s(0))} \approx \m{s(s(s(0)))}}$
  \[
  \frac{
   \makebox[0pt][r]{\structure{$\mathtt{[a]}$}\:}
   \frac{}{\textstyle
   \GREEN{\m{s}(0)+\m{s(0)} \approx \m{s}(0+\m{s}(0))}%
  \rule[-1.5ex]{0pt}{4ex}}
   \quad
   \tfrac{
   \tfrac{}{\textstyle
   \GREEN{\m{0}+\m{s(0)} \approx \m{s(0)}}\rule[-1.5ex]{0pt}{4ex}}
   \makebox[0pt][l]{\:\structure{$\mathtt{[a]}$}}
   }{\textstyle
   \GREEN{\m{s}(0+s\m{(0))} \approx \m{s(s(0))}}\rule[-1.5ex]{0pt}{4ex}}
   \makebox[0pt][l]{\:\structure{$\mathtt{[c]}$}}
  }{
   \frac{\textstyle
   \GREEN{\m{s(0)}+\m{s(0)} \approx \m{s(s(0))}}\rule[-1.5ex]{0pt}{4ex}
   }{\textstyle
   \GREEN{\m{s}(\m{s}(0)+\m{s}(0)) \approx \m{s(s(s(0)))}}%
  \rule[-1.5ex]{0pt}{4ex}}
   \makebox[0pt][l]{\:\structure{$\mathtt{[c]}$}}}
  \makebox[0pt][l]{\:\structure{$\mathtt{[t]}$}}
  \]
  \onslide<2->
  $\GREEN{\m{s(s(0)}+\m{s(0))} \alert<2>{\conv_{\EE}} \m{s(s(s(0)))}}$
  \[
  \GREEN{
  \m{s(s(0)}+\m{s(0))}
  \leftrightarrow_{\EE} \m{s}(\m{s}(\m{0}+\m{s}(\m{0})))
  \leftrightarrow_{\EE} \m{s}(\m{s}(\m{s}(\m{0})))
  }
  \]
  \vspace{-3ex}
  \end{example}
\end{frame}