theorem LO.Modal.Hilbert.KD_weakerThan_KT : LO.Modal.Hilbert.KD ℕ ≤ₛ LO.Modal.Hilbert.KT ℕ

theorem LO.Modal.Hilbert.KD_strictlyWeakerThan_KT : LO.Modal.Hilbert.KD ℕ <ₛ LO.Modal.Hilbert.KT ℕ