∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  {a a_1 : CommRingCat.Colimits.Prequotient F} (t : CommRingCat.Colimits.Relation F a a_1),
  (∀ (x : CommRingCat.Colimits.Prequotient F), motive x x ⋯) →
    (∀ (x y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x y),
        motive x y x_1 → motive y x ⋯) →
      (∀ (x y z : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x y)
          (x_2 : CommRingCat.Colimits.Relation F y z), motive x y x_1 → motive y z x_2 → motive x z ⋯) →
        (∀ (j j' : J) (f : j ⟶ j') (x : ↑(F.obj j)),
            motive (CommRingCat.Colimits.Prequotient.of j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x))
              (CommRingCat.Colimits.Prequotient.of j x) ⋯) →
          (∀ (j : J), motive (CommRingCat.Colimits.Prequotient.of j 0) CommRingCat.Colimits.Prequotient.zero ⋯) →
            (∀ (j : J), motive (CommRingCat.Colimits.Prequotient.of j 1) CommRingCat.Colimits.Prequotient.one ⋯) →
              (∀ (j : J) (x : ↑(F.obj j)),
                  motive (CommRingCat.Colimits.Prequotient.of j (-x)) (CommRingCat.Colimits.Prequotient.of j x).neg ⋯) →
                (∀ (j : J) (x y : ↑(F.obj j)),
                    motive (CommRingCat.Colimits.Prequotient.of j (x + y))
                      ((CommRingCat.Colimits.Prequotient.of j x).add (CommRingCat.Colimits.Prequotient.of j y)) ⋯) →
                  (∀ (j : J) (x y : ↑(F.obj j)),
                      motive (CommRingCat.Colimits.Prequotient.of j (x * y))
                        ((CommRingCat.Colimits.Prequotient.of j x).mul (CommRingCat.Colimits.Prequotient.of j y)) ⋯) →
                    (∀ (x x' : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
                        motive x x' x_1 → motive x.neg x'.neg ⋯) →
                      (∀ (x x' y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
                          motive x x' x_1 → motive (x.add y) (x'.add y) ⋯) →
                        (∀ (x y y' : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F y y'),
                            motive y y' x_1 → motive (x.add y) (x.add y') ⋯) →
                          (∀ (x x' y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
                              motive x x' x_1 → motive (x.mul y) (x'.mul y) ⋯) →
                            (∀ (x y y' : CommRingCat.Colimits.Prequotient F)
                                (x_1 : CommRingCat.Colimits.Relation F y y'),
                                motive y y' x_1 → motive (x.mul y) (x.mul y') ⋯) →
                              (∀ (x : CommRingCat.Colimits.Prequotient F),
                                  motive (CommRingCat.Colimits.Prequotient.zero.add x) x ⋯) →
                                (∀ (x : CommRingCat.Colimits.Prequotient F),
                                    motive (x.add CommRingCat.Colimits.Prequotient.zero) x ⋯) →
                                  (∀ (x : CommRingCat.Colimits.Prequotient F),
                                      motive (CommRingCat.Colimits.Prequotient.one.mul x) x ⋯) →
                                    (∀ (x : CommRingCat.Colimits.Prequotient F),
                                        motive (x.mul CommRingCat.Colimits.Prequotient.one) x ⋯) →
                                      (∀ (x : CommRingCat.Colimits.Prequotient F),
                                          motive (x.neg.add x) CommRingCat.Colimits.Prequotient.zero ⋯) →
                                        (∀ (x y : CommRingCat.Colimits.Prequotient F), motive (x.add y) (y.add x) ⋯) →
                                          (∀ (x y : CommRingCat.Colimits.Prequotient F), motive (x.mul y) (y.mul x) ⋯) →
                                            (∀ (x y z : CommRingCat.Colimits.Prequotient F),
                                                motive ((x.add y).add z) (x.add (y.add z)) ⋯) →
                                              (∀ (x y z : CommRingCat.Colimits.Prequotient F),
                                                  motive ((x.mul y).mul z) (x.mul (y.mul z)) ⋯) →
                                                (∀ (x y z : CommRingCat.Colimits.Prequotient F),
                                                    motive (x.mul (y.add z)) ((x.mul y).add (x.mul z)) ⋯) →
                                                  (∀ (x y z : CommRingCat.Colimits.Prequotient F),
                                                      motive ((x.add y).mul z) ((x.mul z).add (y.mul z)) ⋯) →
                                                    (∀ (x : CommRingCat.Colimits.Prequotient F),
                                                        motive (CommRingCat.Colimits.Prequotient.zero.mul x)
                                                          CommRingCat.Colimits.Prequotient.zero ⋯) →
                                                      (∀ (x : CommRingCat.Colimits.Prequotient F),
                                                          motive (x.mul CommRingCat.Colimits.Prequotient.zero)
                                                            CommRingCat.Colimits.Prequotient.zero ⋯) →
                                                        motive a a_1 t