Documentation

Foundation.Modal.Hilbert.WeakerThan.K_K5

source
theorem LO.Modal.Hilbert.K_strictlyWeakerThan_K5 :
LO.Modal.Hilbert.K ℕ <ₛ LO.Modal.Hilbert.K5 ℕ