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.Kripke.iff_boxdot_reflexive_closure {F : Frame} {φ : Formula ℕ} {V : Valuation F} {x : { toFrame := F, Val := V }.World} : Formula.Kripke.Satisfies { toFrame := F, Val := V } x (φᵇ) ↔ Formula.Kripke.Satisfies { toFrame := F^=, Val := V } x φ

theorem LO.Modal.Kripke.iff_frame_boxdot_reflexive_closure {F : Frame} {φ : Formula ℕ} : F ⊧ φᵇ ↔ F^= ⊧ φ

theorem LO.Modal.Kripke.iff_reflexivize_irreflexivize {F : Frame} {φ : Formula ℕ} [IsRefl F.World F.Rel] {x : F.World} {V : Valuation F} : Formula.Kripke.Satisfies { toFrame := F, Val := V } x φ ↔ Formula.Kripke.Satisfies { toFrame := F^≠^=, Val := V } x φ

theorem LO.Modal.Kripke.iff_reflexivize_irreflexivize' {F : Frame} {φ : Formula ℕ} [IsRefl F.World F.Rel] : F ⊧ φ ↔ F^≠^= ⊧ φ

theorem LO.Modal.Hilbert.provable_boxdotTranslated_GL_of_Grz {φ : Formula ℕ} : Hilbert.Grz ⊢! φ → Hilbert.GL ⊢! φᵇ

theorem LO.Modal.Hilbert.provable_Grz_of_boxdotTranslated_GL {φ : Formula ℕ} : Hilbert.GL ⊢! φᵇ → Hilbert.Grz ⊢! φ

theorem LO.Modal.Hilbert.iff_boxdotTranslatedGL_Grz {φ : Formula ℕ} : Hilbert.GL ⊢! φᵇ ↔ Hilbert.Grz ⊢! φ

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