∀ {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