Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
K_K4
Search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Basic
Imported by
Foundation
LO
.
Modal
.
Hilbert
.
K_strictlyWeakerThan_K4
source
theorem
LO
.
Modal
.
Hilbert
.
K_strictlyWeakerThan_K4
:
Hilbert.K
ℕ
<ₛ
Hilbert.K4
ℕ