{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} →
      {motive : RingCat.Colimits.Prequotient F → Sort u} →
        (t : RingCat.Colimits.Prequotient F) →
          t.ctorIdx = 0 → ((j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x)) → motive t