{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.Cone F} →
            {motive : CategoryTheory.Limits.IsLimit t → Sort u} →
              (t_1 : CategoryTheory.Limits.IsLimit t) →
                ((lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) →
                    (fac :
                        ∀ (s : CategoryTheory.Limits.Cone F) (j : J),
                          CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j) →
                      (uniq :
                          ∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
                            (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s) →
                        motive { lift := lift, fac := fac, uniq := uniq }) →
                  motive t_1