∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) {A : Type u_5} [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] (f : σ → A) (φ : MvPolynomial σ R),
  (MvPolynomial.aeval f) ((MvPolynomial.expand p) φ) = (MvPolynomial.aeval (f ^ p)) φ