∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))