\begin{frame}
  \small
  
  \begin{lemma}
  \smallskip
  The rewrite relation $\to_\atrs$ is the smallest relation on $\TT(\FF,\VV)$ that:
  \begin{itemize}
    \item contains the rules $\RR$,
    \item is closed under context, and
    \item is closed under substitutions.
  \end{itemize}
  That is, $\to_\atrs$ is the closure of $\RR$ under contexts and substitutions.
  \smallskip
  \end{lemma}
\end{frame}