\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
  
  \onslide<2->
  $\EE \vdash \GREEN{\m{s(s(0)}+\m{s(0))} \approx \m{s(s(s(0)))}}$
  \onslide<3->
  \[
  \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]}$}}
  \]
  \end{example}
\end{frame}