{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                {G : CategoryTheory.Functor B D} →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      {motive : G.PreservesLeftKanExtension F L → Sort u} →
                        ((preserves :
                              ∀ (F' : CategoryTheory.Functor C B) (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α],
                                (F'.comp G).IsLeftKanExtension
                                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G)
                                    (L.associator F' G).hom)) →
                            motive ⋯) →
                          (t : G.PreservesLeftKanExtension F L) → motive t