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

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

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

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

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