∀ {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C}
  (f f_1 : Y₁.Hom Y₂),
  (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f =
      CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f_1) =
    (f = f_1)