\begin{frame}{Towards the Compactness Theorem}
  \blockentailment
  \pause\bigskip

  \begin{goal}{}
    \alert{Note:}
    Every natural deduction derivation must be finite.\\
    \pause\smallskip
    
    Hence it can use only finitely many of the premises in $\asetforms$.
  \end{goal}    
\end{frame}