{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {J : Type w} →
      {inst_1 : LinearOrder J} →
        {inst_2 : OrderBot J} →
          {F : CategoryTheory.Functor J C} →
            {c : CategoryTheory.Limits.Cocone F} →
              {X Y : C} →
                {p : X ⟶ Y} →
                  {f : F.obj ⊥ ⟶ X} →
                    {g : c.pt ⟶ Y} →
                      {j : J} →
                        {P : Sort u_1} →
                          {f' : F.obj j ⟶ X} →
                            {w₁ :
                                autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
                                  CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam} →
                              {w₂ :
                                  autoParam
                                    (CategoryTheory.CategoryStruct.comp f' p =
                                      CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
                                    CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam} →
                                {f'' : F.obj j ⟶ X} →
                                  {w₁' :
                                      autoParam
                                        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f'' = f)
                                        CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam} →
                                    {w₂' :
                                        autoParam
                                          (CategoryTheory.CategoryStruct.comp f'' p =
                                            CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
                                          CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam} →
                                      { f' := f', w₁ := w₁, w₂ := w₂ } = { f' := f'', w₁ := w₁', w₂ := w₂' } →
                                        (f' ≍ f'' → P) → P