∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) (s : Finset ℕ) (g : ℕ → R) ⦃x : ℕ⦄
  (motive : x ∈ {i | i ∈ s ∧ g i • ↑S i ≠ 0} → Prop) (h : x ∈ {i | i ∈ s ∧ g i • ↑S i ≠ 0}),
  (∀ (left : x ∈ s) (hx : g x • ↑S x ≠ 0), motive ⋯) → motive h