theorem LO.Modal.Hilbert.KT_weakerThan_KTB {α : Type u_1} : LO.Modal.Hilbert.KT α ≤ₛ LO.Modal.Hilbert.KTB α

theorem LO.Modal.Hilbert.KT_strictlyWeakerThan_KTB : LO.Modal.Hilbert.KT ℕ <ₛ LO.Modal.Hilbert.KTB ℕ