Documentation

Foundation.Modal.Hilbert.WeakerThan.K_KD

source
theorem LO.Modal.Hilbert.K_strictlyWeakerThan_KD :
LO.Modal.Hilbert.K ℕ <ₛ LO.Modal.Hilbert.KD ℕ