{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            {motive : CategoryTheory.Limits.IsColimit t → Sort u} →
              (t_1 : CategoryTheory.Limits.IsColimit t) →
                ((desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) →
                    (fac :
                        ∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
                          CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j) →
                      (uniq :
                          ∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
                            (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s) →
                        motive { desc := desc, fac := fac, uniq := uniq }) →
                  motive t_1