\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}