{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J CommRingCat} →
      {motive : CommRingCat.Colimits.Prequotient F → Sort u} →
        (t : CommRingCat.Colimits.Prequotient F) →
          t.ctorIdx = 4 → ((a a_1 : CommRingCat.Colimits.Prequotient F) → motive (a.add a_1)) → motive t