theorem LO.Modal.Logic.iff_provable_rflSubformula_GL_provable_S {φ : Formula ℕ} : Modal.GL ⊢ Finset.conj φ.rflSubformula ➝ φ ↔ Modal.S ⊢ φ

theorem LO.Modal.Logic.iff_provable_boxdot_GL_provable_boxdot_S {φ : Formula ℕ} : Modal.GL ⊢ φᵇ ↔ Modal.S ⊢ φᵇ