theorem LO.Modal.Hilbert.K5_weakerThan_KD5 {α : Type u_1} : LO.Modal.Hilbert.K5 α ≤ₛ LO.Modal.Hilbert.KD5 α

theorem LO.Modal.Hilbert.K5_strictlyWeakerThan_KD5 : LO.Modal.Hilbert.K5 ℕ <ₛ LO.Modal.Hilbert.KD5 ℕ