{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 = 5 → ((a a_1 : RingCat.Colimits.Prequotient F) → motive (a.mul a_1)) → motive t