def LO.System.KP.axiomD {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.KP 𝓢] {φ : F} [LO.System.HasDiaDuality 𝓢] : 𝓢 ⊢ LO.Axioms.D φ

Equations

• One or more equations did not get rendered due to their size.

instance LO.System.KP.instHasAxiomD {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.KP 𝓢] : LO.System.HasAxiomD 𝓢

Equations

• LO.System.KP.instHasAxiomD = { D := fun (x : F) => LO.System.KP.axiomD }