\begin{frame}
  \frametitle{Towards a Proof of Combinatorial Completeness}

  \begin{lemma}[Properties of ]
  \begin{enumerate}
  \item $([x]t)x\to^* t$
  \item The variable $x$ does not occur in the CL-term denoted by $[x]t$\pause
  \end{enumerate}
  \end{lemma}

  \begin{proof}  
  Induction on  $t$:
  
  \begin{description}
  \item[base case] $([x]x)x = Ix \to x$
  
  $([x]y)x = Kyx \to y$
  (the same if $t$ is a constant)\pause
  
  \item[induction] IH: $([x]t)x\to^* t$ and $([x]t')x\to^* t'$\pause
  %
  \begin{align*}
  ([x]tt')x 
  &= S([x]t)([x]t')x 
  \to ([x]t)x(([x]t')x) \\
  &\to^* t(([x]t')x)
  \to^* tt'
  \end{align*}
  \vspace{-5ex}
  \end{description}
  \end{proof}  
\end{frame}