 Crucially, then, with regard to such KQML validities as \(\forall \sfx(\sfF\sfx \to \sfF\sfx)\) and \(\forall \sfx\,\Box(\Box \sfF\sfx \to \sfF\sfx)\) that are derivable in SQML by applications of Gen and Nec, instances of the above schemas can contain free variable occurrences. So, in particular, \(\forall \sfx(\sfF\sfx \to \sfF\sfx)\) is a closure of the propositional tautology \(\sfF\sfx \to \sfF\sfx,\) and \(\forall \sfx\,\Box(\Box \sfF\sfx \to \sfF\sfx)\) is a closure of the T instance \(\Box \sfF\sfx \to \sfF\sfx\) and, hence, both validities are axioms (hence theorems) of KQML.