∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R),
        a ∉ f.support →
          b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b) → motive ((MvPolynomial.monomial a) b + f)) →
      (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) → motive p