∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} {t : CategoryTheory.Limits.IsColimit c}
  (toLiftableCocone : CategoryTheory.LiftableCocone K F c)
  (makesColimit : CategoryTheory.Limits.IsColimit toLiftableCocone.liftedCocone)
  (toLiftableCocone_1 : CategoryTheory.LiftableCocone K F c)
  (makesColimit_1 : CategoryTheory.Limits.IsColimit toLiftableCocone_1.liftedCocone),
  ({ toLiftableCocone := toLiftableCocone, makesColimit := makesColimit } =
      { toLiftableCocone := toLiftableCocone_1, makesColimit := makesColimit_1 }) =
    (toLiftableCocone = toLiftableCocone_1 ∧ makesColimit ≍ makesColimit_1)