∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} {a a_1 : X.Hom Y}
  (t : CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1),
  (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y), motive f f ⋯) →
    (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f g : X.Hom Y)
        (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f g), motive g f ⋯) →
      (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} {f g h : X.Hom Y}
          (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f g)
          (a_2 : CategoryTheory.FreeMonoidalCategory.HomEquiv g h), motive f h ⋯) →
        (∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : X.Hom Y} {g g' : Y.Hom Z}
            (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f')
            (a_2 : CategoryTheory.FreeMonoidalCategory.HomEquiv g g'), motive (f.comp g) (f'.comp g') ⋯) →
          (∀ (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C} (f f' : Y.Hom Z)
              (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f'),
              motive (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f)
                (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f') ⋯) →
            (∀ {Y Z : CategoryTheory.FreeMonoidalCategory C} (f f' : Y.Hom Z)
                (X : CategoryTheory.FreeMonoidalCategory C) (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f'),
                motive (f.whiskerRight X) (f'.whiskerRight X) ⋯) →
              (∀ {W X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : W.Hom X} {g g' : Y.Hom Z}
                  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f')
                  (a_2 : CategoryTheory.FreeMonoidalCategory.HomEquiv g g'), motive (f.tensor g) (f'.tensor g') ⋯) →
                (∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : X₁.Hom Y₁) (g : X₂.Hom Y₂),
                    motive (f.tensor g)
                      ((f.whiskerRight X₂).comp (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft Y₁ g)) ⋯) →
                  (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
                      motive (f.comp (CategoryTheory.FreeMonoidalCategory.Hom.id Y)) f ⋯) →
                    (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
                        motive ((CategoryTheory.FreeMonoidalCategory.Hom.id X).comp f) f ⋯) →
                      (∀ {X Y U V : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom U) (g : U.Hom V) (h : V.Hom Y),
                          motive ((f.comp g).comp h) (f.comp (g.comp h)) ⋯) →
                        (∀ {X Y : CategoryTheory.FreeMonoidalCategory C},
                            motive
                              ((CategoryTheory.FreeMonoidalCategory.Hom.id X).tensor
                                (CategoryTheory.FreeMonoidalCategory.Hom.id Y))
                              (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y)) ⋯) →
                          (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁)
                              (f₂ : X₂.Hom Y₂) (g₁ : Y₁.Hom Z₁) (g₂ : Y₂.Hom Z₂),
                              motive ((f₁.tensor f₂).comp (g₁.tensor g₂)) ((f₁.comp g₁).tensor (f₂.comp g₂)) ⋯) →
                            (∀ (X Y : CategoryTheory.FreeMonoidalCategory C),
                                motive
                                  (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X
                                    (CategoryTheory.FreeMonoidalCategory.Hom.id Y))
                                  (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y)) ⋯) →
                              (∀ (X Y : CategoryTheory.FreeMonoidalCategory C),
                                  motive ((CategoryTheory.FreeMonoidalCategory.Hom.id X).whiskerRight Y)
                                    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y)) ⋯) →
                                (∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C},
                                    motive
                                      ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z).comp
                                        (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z))
                                      (CategoryTheory.FreeMonoidalCategory.Hom.id ((X.tensor Y).tensor Z)) ⋯) →
                                  (∀ {X Y Z : CategoryTheory.FreeMonoidalCategory C},
                                      motive
                                        ((CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z).comp
                                          (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z))
                                        (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor (Y.tensor Z))) ⋯) →
                                    (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CategoryTheory.FreeMonoidalCategory C} (f₁ : X₁.Hom Y₁)
                                        (f₂ : X₂.Hom Y₂) (f₃ : X₃.Hom Y₃),
                                        motive
                                          (((f₁.tensor f₂).tensor f₃).comp
                                            (CategoryTheory.FreeMonoidalCategory.Hom.α_hom Y₁ Y₂ Y₃))
                                          ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X₁ X₂ X₃).comp
                                            (f₁.tensor (f₂.tensor f₃)))
                                          ⋯) →
                                      (∀ {X : CategoryTheory.FreeMonoidalCategory C},
                                          motive
                                            ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X).comp
                                              (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X))
                                            (CategoryTheory.FreeMonoidalCategory.Hom.id
                                              (X.tensor CategoryTheory.FreeMonoidalCategory.unit))
                                            ⋯) →
                                        (∀ {X : CategoryTheory.FreeMonoidalCategory C},
                                            motive
                                              ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X).comp
                                                (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X))
                                              (CategoryTheory.FreeMonoidalCategory.Hom.id X) ⋯) →
                                          (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
                                              motive
                                                ((f.whiskerRight CategoryTheory.FreeMonoidalCategory.unit).comp
                                                  (CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom Y))
                                                ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom X).comp f) ⋯) →
                                            (∀ {X : CategoryTheory.FreeMonoidalCategory C},
                                                motive
                                                  ((CategoryTheory.FreeMonoidalCategory.Hom.l_hom X).comp
                                                    (CategoryTheory.FreeMonoidalCategory.Hom.l_inv X))
                                                  (CategoryTheory.FreeMonoidalCategory.Hom.id
                                                    (CategoryTheory.FreeMonoidalCategory.unit.tensor X))
                                                  ⋯) →
                                              (∀ {X : CategoryTheory.FreeMonoidalCategory C},
                                                  motive
                                                    ((CategoryTheory.FreeMonoidalCategory.Hom.l_inv X).comp
                                                      (CategoryTheory.FreeMonoidalCategory.Hom.l_hom X))
                                                    (CategoryTheory.FreeMonoidalCategory.Hom.id X) ⋯) →
                                                (∀ {X Y : CategoryTheory.FreeMonoidalCategory C} (f : X.Hom Y),
                                                    motive
                                                      ((CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft
                                                            CategoryTheory.FreeMonoidalCategory.unit f).comp
                                                        (CategoryTheory.FreeMonoidalCategory.Hom.l_hom Y))
                                                      ((CategoryTheory.FreeMonoidalCategory.Hom.l_hom X).comp f) ⋯) →
                                                  (∀ {W X Y Z : CategoryTheory.FreeMonoidalCategory C},
                                                      motive
                                                        (((CategoryTheory.FreeMonoidalCategory.Hom.α_hom W X
                                                                  Y).whiskerRight
                                                              Z).comp
                                                          ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom W (X.tensor Y)
                                                                Z).comp
                                                            (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft W
                                                              (CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z))))
                                                        ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom (W.tensor X) Y
                                                              Z).comp
                                                          (CategoryTheory.FreeMonoidalCategory.Hom.α_hom W X
                                                            (Y.tensor Z)))
                                                        ⋯) →
                                                    (∀ {X Y : CategoryTheory.FreeMonoidalCategory C},
                                                        motive
                                                          ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X
                                                                CategoryTheory.FreeMonoidalCategory.unit Y).comp
                                                            (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X
                                                              (CategoryTheory.FreeMonoidalCategory.Hom.l_hom Y)))
                                                          ((CategoryTheory.FreeMonoidalCategory.Hom.ρ_hom
                                                                X).whiskerRight
                                                            Y)
                                                          ⋯) →
                                                      motive a a_1 t