@[reducible, inline]

abbrev LO.Modal.Kripke.UniversalFrameClass : FrameClass

Equations

• LO.Modal.Kripke.UniversalFrameClass = {F : LO.Modal.Kripke.Frame | Universal F.Rel}

theorem LO.Modal.Kripke.iff_Universal_ReflexiveEuclidean_validOnFrameClass {φ : Formula ℕ} : UniversalFrameClass ⊧ φ ↔ ReflexiveEuclideanFrameClass ⊧ φ

instance LO.Modal.Hilbert.S5.Kripke.complete_universal : Complete (Hilbert.S5 ℕ) Kripke.UniversalFrameClass