Equations
- LO.Modal.Standard.Kripke.axiomL_definability = { define := ⋯, nonempty := LO.Modal.Standard.Kripke.axiomL_definability.proof_2 }
instance
LO.Modal.Standard.Kripke.instConsistentFormulaDeductionParameterGL
{α : Type u}
[Inhabited α]
:
Equations
- ⋯ = ⋯
Equations
- LO.Modal.Standard.Kripke.axiomL_finite_definability = { define := ⋯, nonempty := LO.Modal.Standard.Kripke.axiomL_finite_definability.proof_2 }
Equations
- ⋯ = ⋯