theorem LO.Modal.Hilbert.K4_weakerThan_KD4 {α : Type u_1} : Hilbert.K4 α ≤ₛ Hilbert.KD4 α

theorem LO.Modal.Hilbert.K4_strictlyWeakerThan_KD4 : Hilbert.K4 ℕ <ₛ Hilbert.KD4 ℕ