{C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    (F A : CategoryTheory.Functor C (Type u_2)) →
      (X : C) →
        (motive : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X → Sort u_4) →
          (x : (CategoryTheory.MonoidalCategoryStruct.tensorObj F A).obj X) →
            ((x : F.obj X) → (y : A.obj X) → motive (x, y)) → motive x