theorem LO.Modal.Hilbert.KT_weakerThan_S4 {α : Type u_1} : Hilbert.KT α ≤ₛ Hilbert.S4 α

theorem LO.Modal.Hilbert.KT_strictlyWeakerThan_S4 : Hilbert.KT ℕ <ₛ Hilbert.S4 ℕ