∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y Z : CategoryTheory.FreeMonoidalCategory C} {f f' : X.Hom Y} {g g' : Y.Hom Z}
  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f') (a_1 : CategoryTheory.FreeMonoidalCategory.HomEquiv g g'),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f f' a →
      CategoryTheory.FreeMonoidalCategory.HomEquiv.below a_1 →
        motive g g' a_1 → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯