theorem LO.Modal.Hilbert.K4_weakerThan_GL {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.K4 α ≤ₛ LO.Modal.Hilbert.GL α

theorem LO.Modal.Hilbert.K4_strictlyWeakerThan_GL : LO.Modal.Hilbert.K4 ℕ <ₛ LO.Modal.Hilbert.GL ℕ