∀ {M : Type u_1} (R : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c = d) (x : R),
  (RingCon.congr h).toFun ((algebraMap R c.Quotient) x) = (RingCon.congr h).toFun ((algebraMap R c.Quotient) x)