∀ {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)}
  (liftedCocone : CategoryTheory.Limits.Cocone K) (validLift : F.mapCocone liftedCocone ≅ c)
  (liftedCocone_1 : CategoryTheory.Limits.Cocone K) (validLift_1 : F.mapCocone liftedCocone_1 ≅ c),
  ({ liftedCocone := liftedCocone, validLift := validLift } =
      { liftedCocone := liftedCocone_1, validLift := validLift_1 }) =
    (liftedCocone = liftedCocone_1 ∧ validLift ≍ validLift_1)