theorem LO.Modal.Hilbert.admissible_subst! {α : Type u_1} [DecidableEq α] {H : LO.Modal.Hilbert α} [H.IsNormal] {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} [H.axioms.SubstClosed] (d : H ⊢! φ) : H ⊢! LO.Modal.Formula.subst σ φ

instance LO.Modal.Hilbert.instSubstClosedSetFormula {α : Type u_1} : LO.Modal.Theory.SubstClosed 𝗞

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instSubstClosedSetFormula_1 {α : Type u_1} : LO.Modal.Theory.SubstClosed 𝗟

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instSubstClosedSetFormula_2 {α : Type u_1} : LO.Modal.Theory.SubstClosed 𝗚𝗿𝘇

Equations

• ⋯ = ⋯

instance LO.Modal.Hilbert.instSubstClosedSetFormula_3 {α : Type u_1} : LO.Modal.Theory.SubstClosed 𝗛

Equations

• ⋯ = ⋯