\begin{frame}
  \small
  
  \begin{definition}
  \begin{itemize}
  \item
  \makebox[3cm][l]{\alert<1,2>{diamond property}}
  \onslide<3->{\alert<3>{$\diamond$}}
  \begin{itemize}
  \item
  ${\from \cdot \to} \:\subseteq\: {\to \cdot \from}$
  \smallskip
  \item<2->
  \hspace{-1mm}\begin{tikzpicture}[on grid,baseline=(1).baseline]
  \node (1)                    {$\strut a$};
  \node (2) [below left=of 1]  {$b$};
  \node (3) [below right=of 1] {$c$};
  \node (4) [below right=of 2] {$\strut d$};
  \node (5) [left=of 1]        {\makebox[3cm][l]{$\strut \forall a,b,c$}};
  \node (6) [left=of 4]        {\makebox[3cm][l]{$\strut \exists d$}};
  \draw[->]        (1) -- (2);
  \draw[->]        (1) -- (3);
  \draw[dotted,->] (2) -- (4);
  \draw[dotted,->] (3) -- (4);
  \end{tikzpicture}
  \end{itemize}
  \end{itemize}
  \end{definition}
  
  \bigskip
  
  \begin{lemma}<4->
  \smallskip
  An ARS $\AA = \ARS$ is confluent if ${\to}$ has the diamond property.
  \smallskip
  \end{lemma}

  \onslide<5->
  \begin{proof}  
  Exercise.
  \end{proof}  
\end{frame}