theorem LO.Modal.Kripke.mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass {F : Frame} (hF : F ∈ FrameClass.finite_trans_irrefl) : F^= ∈ FrameClass.finite_partial_order

theorem LO.Modal.Kripke.mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass {F : Frame} (hF : F ∈ FrameClass.finite_partial_order) : F^≠ ∈ FrameClass.finite_trans_irrefl

theorem LO.Modal.Logic.provable_boxdot_GL_of_provable_Grz {φ : Formula ℕ} : φ ∈ Logic.Grz → φᵇ ∈ Logic.GL

theorem LO.Modal.Logic.provable_Grz_of_provable_boxdot_GL {φ : Formula ℕ} : φᵇ ∈ Logic.GL → φ ∈ Logic.Grz

theorem LO.Modal.Logic.iff_provable_boxdot_GL_provable_Grz {φ : Formula ℕ} : φᵇ ∈ Logic.GL ↔ φ ∈ Logic.Grz

instance LO.Modal.Logic.instBoxdotPropertyGLGrz : BoxdotProperty Logic.GL Logic.Grz