Supports in the same orbit

theorem ConNF.Spec.Specifies.smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {S : ConNF.Support ↑β} {hS : S.Strong} {σ : ConNF.Spec β} (hσS : σ.Specifies S hS) (ρ : ConNF.Allowable ↑β) : σ.Specifies (ρ • S) ⋯