∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R),
  (MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) =
    MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.map f) ∘ g) ((MvPolynomial.map f) p)