@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.corefl : FrameClass

Equations

• LO.Modal.Kripke.FrameClass.corefl = {F : LO.Modal.Kripke.Frame | IsCoreflexive F.World F.Rel}

instance LO.Modal.Hilbert.KTc.Kripke.sound : Sound Hilbert.KTc Kripke.FrameClass.corefl

instance LO.Modal.Hilbert.KTc.Kripke.consistent : Entailment.Consistent Hilbert.KTc

instance LO.Modal.Hilbert.KTc.Kripke.canonical : Kripke.Canonical Hilbert.KTc Kripke.FrameClass.corefl

instance LO.Modal.Hilbert.KTc.Kripke.complete : Complete Hilbert.KTc Kripke.FrameClass.corefl