\begin{frame}[t]
  \frametitle{Case (a): Disjoint redexes}

  \begin{minipage}{.5\textwidth}
  \includegraphics[width=.90\textwidth]{../graphics/critpairlemma}
  \end{minipage}
  \begin{minipage}{.49\textwidth}
  Assume $s_0$ {and} $s_1$ are \alert{disjoint}.
  \pause\bigskip
  
  Then $t= C[s_0,s_1]$\\
  for some $2$-hole context $C$.
  \pause\bigskip
  
  Let $s_0'$, $s_1'$ be the
  contracta of $s_0$, $s_1$.
  \bigskip\pause
  
  Then $t_0 = C[s_0',s_1]$ and $t_1 = C[s_0,s_1']$.
  \bigskip\pause
  
  Take $t_2 = C[s_0',s_1']$ as common reduct.
  \end{minipage}
\end{frame}