∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop},
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) →
      ∀ (s : σ →₀ ℕ) (a : R), motive ((MvPolynomial.monomial s) a)