\begin{frame}
  \small
  
  \begin{block}{Inference Rules}<+->
  \begin{itemize}
  \item[\structure{$\mathtt{[r]}$}] \quad
  \makebox[25mm][l]{\alert<1>{reflexivity}}
  \makebox[45mm][c]{$\displaystyle
  \frac{\phantom{s \approx t}}{t \approx t}$}
  $\forall$ $t$
  \medskip
  \item<2->[\structure{$\mathtt{[s]}$}] \quad
  \makebox[25mm][l]{\alert<2>{symmetry}}
  \makebox[45mm][c]{$\displaystyle
  \frac{s \approx t}{t \approx s}$}
  \medskip
  \item<3->[\structure{$\mathtt{[t]}$}] \quad
  \makebox[25mm][l]{\alert<3>{transitivity}}
  \makebox[45mm][c]{$\displaystyle
  \frac{s \approx t,\:t \approx u}{s \approx u}$}
  \smallskip
  \item<4->[\structure{$\mathtt{[a]}$}] \quad
  \makebox[25mm][l]{\alert<4>{application}}
  \makebox[45mm][c]{$\displaystyle
  \frac{\phantom{s \approx t}}{l\sigma \approx r\sigma}$}
  $\forall$ $l \approx r \in \EE$ $\forall$ $\sigma$
  \medskip
  \item<5->[\structure{$\mathtt{[c]}$}] \quad
  \makebox[25mm][l]{\alert<5>{congruence}}
  \makebox[45mm][c]{$\displaystyle
  \frac{s_1 \approx t_1,\:\dots,\:s_n \approx t_n}
  {f(\seq{s}) \approx f(\seq{t})}$}
  $\forall$ $n$-ary $f$
  \end{itemize}
  \end{block}
  
  \medskip
  
  \begin{definition}<6->
  \smallskip
  \alert<6>{$\EE \vdash s \approx t$} \quad (\alert<6>{$s \approx_\EE t$})\quad
  if equation $s \approx t$ is derivable.
  \end{definition}
\end{frame}