instance LO.Modal.Kripke.Model.instIsTransitivePointGenerate {M : Model} {x : M.World} [M.IsTransitive] : (M↾x).IsTransitive

instance LO.Modal.Kripke.Model.instIsTransitiveExtendRoot {M : Model} {n : ℕ+} [M.IsTransitive] [M.IsPointRooted] : (M.extendRoot n).IsTransitive

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 ⊢ φᵇ