Documentation

Foundation.Modal.Hilbert.WeakerThan.K_KB

source
theorem LO.Modal.Hilbert.K_strictlyWeakerThan_KB :
Hilbert.K ℕ <ₛ Hilbert.KB ℕ