theorem LO.Modal.Hilbert.K4_weakerThan_S4 {α : Type u_1} : LO.Modal.Hilbert.K4 α ≤ₛ LO.Modal.Hilbert.S4 α

theorem LO.Modal.Hilbert.K4_strictlyWeakerThan_S4 : LO.Modal.Hilbert.K4 ℕ <ₛ LO.Modal.Hilbert.S4 ℕ