\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}