noncomputable def ConNF.Support.spec [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) (hS : S.Strong) : ConNF.Spec β

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Support.spec_specifies [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (S : ConNF.Support ↑β) (hS : S.Strong) : (S.spec hS).Specifies S hS