\begin{frame}
  \frametitle{Simulation of beta reduction}


  \begin{lemma}{}
  We can use abstraction to simulate $\beta$-reduction of $\lambda$-calculus:
  \begin{align*}
    ([x]t)t'\to^* t[x:=t']
  \end{align*}
  \end{lemma}
  \pause
  \bigskip
  \begin{proof}  
  We have $([x]t)x\to^* t$.
  
  Substitute $t'$ for $x$ in this reduction.
  \end{proof}  
\end{frame}