Documentation

Foundation.Modal.Hilbert.Equiv.S5_KT4B

source
theorem LO.Modal.Hilbert.equiv_S5_KT4B :
LO.Modal.Hilbert.S5 ℕ =ₛ LO.Modal.Hilbert.KT4B ℕ