∀ (σ : Type u_2) {D : Type u_1} [inst : CommRing D] (s : Finset σ) (w : Multiset (MvPolynomial (↥s) D))
  (b : MvPolynomial σ D) (motive : (∃ a ∈ w, (MvPolynomial.rename Subtype.val) a = b) → Prop)
  (x : ∃ a ∈ w, (MvPolynomial.rename Subtype.val) a = b),
  (∀ (b' : MvPolynomial (↥s) D) (hb' : b' ∈ w) (he : (MvPolynomial.rename Subtype.val) b' = b), motive ⋯) → motive x