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

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