{V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {motive : CategoryTheory.EnrichedFunctor V C D → Sort u} →
                (t : CategoryTheory.EnrichedFunctor V C D) →
                  ((obj : C → D) →
                      (map : (X Y : C) → (X ⟶[V] Y) ⟶ obj X ⟶[V] obj Y) →
                        (map_id :
                            ∀ (X : C),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (map X X) =
                                CategoryTheory.eId V (obj X)) →
                          (map_comp :
                              ∀ (X Y Z : C),
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (map X Z) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (map X Y) (map Y Z))
                                    (CategoryTheory.eComp V (obj X) (obj Y) (obj Z))) →
                            motive { obj := obj, map := map, map_id := map_id, map_comp := map_comp }) →
                    motive t