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