\begin{frame}
  \small
  
  \begin{theorem}[Huet 1980]
  \smallskip
  $\,\text{left-linearity} \quad\&\quad {\cp} \:\subseteq\: \smash{\parr}
  \quad\Longrightarrow\quad \text{CR}$
  \end{theorem}
  
  \begin{proof}<2->[Proof Sketch]
  \begin{itemize}
  \item
  ${\mparr \cdot \parr} \subseteq {\parr \cdot \mparr}$
  \vspace{-3ex}
  \begin{center}
  \begin{tikzpicture}[on grid,node distance=9mm]
  \node (1)              {$\cdot$};
  \node (2) [right=of 1] {\alt<3->{$\cdot$}{}};
  \node (3) [right=of 2] {};
  \node (4) [right=of 3] {$\cdot$};
  \node (4a) [below=of 4] {};
  \node (4b) [below=of 4a] {};
  \alt<3->{
  \draw[->] (1) -- (2);
  \draw[->] (2) -- (4) node[midway] {$\|$};
  }{
  \draw[->] (1) -- (4) node[midway] {$\|$};
  }
  \node (1a) [below=of 1] {\alt<3->{$\cdot$}{}};
  \node (1b) [below=of 1a] {};
  \node (1c) [below=of 1b] {$\cdot$};
  \alt<3->{
  \draw[->] (1) -- (1a);
  \draw[->] (1a) -- (1c) node[midway,sloped] {$\|$};
  }{
  \draw[->] (1) -- (1c) node[midway,sloped] {$\|$};
  }
  \onslide<4->{
  \draw[->] (1a) -- (2) node[midway,sloped] {$\|$};
  }
  \onslide<5->{
  \draw[->] (1a) -- (4) node[midway,sloped] {$\|$};
  }
  \onslide<6->{
  \node (4c) [below=of 4b] {$\cdot$};
  \draw[->] (4) -- (4c) node[midway,sloped] {$\|$};
  \draw[->] (1c) -- (4c) node[midway] {$\|$};
  \path (1) -- (4c) node[midway,anchor=north] {IH};
  }
  \end{tikzpicture}
  \qquad
  \raisebox{15mm}{\onslide<3->{\makebox[0mm][l]{interesting case}}}
  \end{center}
  \vspace{-3ex}
  \item<7->
  ${\to} \subseteq {\parr} \subseteq {\to^*}$
  \smallskip
  \end{itemize}
  \vspace{-3ex}
  \end{proof}
  
  \begin{block}<8->{Open Problem}
  \smallskip
  \it
  $\,\text{left-linearity} \quad\&\quad {\cp} \:\subseteq\: {\mparr}
  \quad\Longrightarrow\quad \text{CR}$ ?
  \end{block}
\end{frame}