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