∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R))
  (x y : R),
  Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.evalEval x y p)