Documentation

Foundation.Modal.Entailment.EMCN

source
instance LO.Modal.Entailment.instKOfEMCN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.EMCN 𝓢] :
Entailment.K 𝓢
Equations
  • One or more equations did not get rendered due to their size.
source
instance LO.Modal.Entailment.instEMCNOfK {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.K 𝓢] :
Entailment.EMCN 𝓢
Equations
  • One or more equations did not get rendered due to their size.