 Much like the instances of Q2, then, because \(\sfE!\tau\) is an axiom of A for any term \(\tau,\) singular instances of \(\Box\Diamond\) fall out as contingent theorems of A. By the observation above, wholly general instances of \(\Box\Diamond_A\) are simply instances of \(\Box\Diamond\) and, hence, their necessitations are provable.