 and the intended proof to BF* stalls out. To continue along the lines of the SQML proof above we would need to be able to swap the initial necessity operator \(\Box\) in line 2* with the universal quantifier to infer