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