∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (p : MvPolynomial σ R), MvPolynomial.eval₂ f g p = (MvPolynomial.eval g) ((MvPolynomial.map f) p)