def LO.System.KP.axiomD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.KP 𝓢] {φ : F} [HasDiaDuality 𝓢] : 𝓢 ⊢ 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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.KP 𝓢] : HasAxiomD 𝓢

Equations

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