∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] {I : Ideal R} {a : MvPolynomial σ R},
  a ∈ Ideal.map MvPolynomial.C I →
    (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) a = 0