\begin{frame}
  \begin{lemma}
    Let $\AA$ well-founded monotone $\Sigma$-algebra.
    Then $>_\AA$ is closed under contexts.
  \end{lemma}
  \pause
   
  \begin{proof}
    Let $s,t \in \TTlong$ such that $t >_\AA s$. \pause
    We show $C[s] >_\AA C[t]$ for every $C[\;]$.\pause\smallskip
    
    That is: $[C[t],\alpha] > [C[s],\alpha]$ for every $\alpha : \VV \to A$.\pause\smallskip
    
    Let $\alpha : \VV \to A$. \pause We show $[C[t],\alpha] > [C[s],\alpha]$ by induction over structure of $C[\;]$:
    \vspace{-.6em}
    \begin{align*}
      \onslide<7-> C[\;] \equiv [\;] \Rightarrow\ &\onslide<8->\interpret{C[t],\alpha} = \interpret{t,\alpha} > \interpret{s,\alpha} = \interpret{C[s],\alpha}\\
      \onslide<9->C[\;] \equiv f(t_1,\ldots,t_n) \Rightarrow\ 
        &\onslide<10->\text{Let $i$ such that $t_i$ contains the hole $\Box$.}\\
        &\onslide<11->\text{Then $C[u] = f(t_1,\ldots,t_i[u],\ldots,t_n)$. Hence}\\
        &\onslide<12->\text{\quad$[C[s],\alpha] = [f]([t_1,\alpha],\ldots,[t_i[s],\alpha],\ldots,[t_n,\alpha])$.}\\
        &\onslide<13->\text{\quad$[C[t],\alpha] = [f]([t_1,\alpha],\ldots,[t_i[t],\alpha],\ldots,[t_n,\alpha])$.}\\
        &\onslide<14->\text{By IH $\interpret{t_i[t],\alpha} > \interpret{t_i[s],\alpha}$}.\\
        &\onslide<15->\text{By monotonicity $\interpret{C[t],\alpha} > \interpret{C[s],\alpha}$.}
    \end{align*}
  \end{proof}
\end{frame}