28/129
\begin{frame}
  \frametitle{Combinatorial Completeness}

  \begin{lemma}[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{lemma}
  \pause
  \bigskip
  
  \onslide<3->{Then closure under substitutions yields:}
  \begin{lemma}
  Then $F\, t_1 \ldots t_n \to^* t[x_1 \mapsto t_1, \dots x_n \mapsto t_n]$
  for arbitrary terms $t_1,\ldots,t_n$.
  \end{lemma}
\end{frame}