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

  \begin{block}{Combinatorial Completeness}
    Given  CL-term $t$, one can find a CL-term $F$ without variables such that  
    
    
    $$Fx_1\ldots x_n\to^* t$$
  \end{block}
  
  \pause
  \bigskip
  \begin{proof}
  Let $x_1,\ldots,x_n$ contain all variables in $t$ (possibly more).
  Let $$F= [x_1x_2\ldots x_n]t$$\pause
  By former proposition and induction on $n$:
  \begin{align*}
  Fx_1\ldots x_n = ([x_1][x_2\ldots x_n]t)x_1\ldots x_n\to^* 
  ([x_2\ldots x_n]t)x_2\ldots x_n \to^* t
  \end{align*}
  \end{proof}
\end{frame}