∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) {B : Type u_2} [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (φ : S₁ →ₐ[R] B) (p : MvPolynomial σ R),
  φ ((MvPolynomial.aeval f) p) = (MvPolynomial.aeval fun i => φ (f i)) p