\begin{frame}
  
  \begin{lemma}
    Let $\AA$ well-founded monotone $\Sigma$-algebra.
    Then $>_\AA$ is well-founded.
  \end{lemma}
  \pause
  
  \begin{proof}
    Assume there is an infinite sequence $t_1 >_\AA t_2 >_\AA t_3 >_\AA \ldots$.\pause\smallskip
    
    Let $\alpha : \VV \to A$. Then by definition of $>_\AA$:
    $[t_1,\alpha] > [t_2,\alpha] > [t_3,\alpha] > \ldots$.\pause\smallskip
    
    This infinite decreasing $>$ chain contradicts well-foundedness of $>$.
  \end{proof}
  \pause
  
  We have shown that:
  \begin{itemize}
  \pause
    \item $>_\AA$ is closed under substitutions
  \pause
    \item $>_\AA$ is closed under contexts
  \pause
    \item $>_\AA$ is well-founded
  \end{itemize} 
  \pause
  
  Hence we have proven that:
  \begin{lemma}
  \smallskip
  $>_\AA$ is a reduction order for every well-founded monotone $\Sigma$-algebra
  $(A,\lbrack \cdot \rbrack,{>})$
  \end{lemma}
\end{frame}