∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.mul CommRingCat.Colimits.Prequotient.one) x