theorem LO.Modal.Hilbert.KD_weakerThan_KDB {α : Type u_1} : LO.Modal.Hilbert.KD α ≤ₛ LO.Modal.Hilbert.KDB α

theorem LO.Modal.Hilbert.KD_strictlyWeakerThan_KDB : LO.Modal.Hilbert.KD ℕ <ₛ LO.Modal.Hilbert.KDB ℕ