∀ (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] (C : Type u_3) [inst_3 : CategoryTheory.EnrichedCategory V C]
  (x x_1 : Cᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.unop x_1 ⟶[V] Opposite.unop x)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.unop x_1 ⟶[V] Opposite.unop x)
          (CategoryTheory.EnrichedCategory.id (Opposite.unop x_1)))
        (CategoryTheory.CategoryStruct.comp
          (β_ (Opposite.unop x_1 ⟶[V] Opposite.unop x) (Opposite.unop x_1 ⟶[V] Opposite.unop x_1)).hom
          (CategoryTheory.EnrichedCategory.comp (Opposite.unop x_1) (Opposite.unop x_1) (Opposite.unop x)))) =
    CategoryTheory.CategoryStruct.id (Opposite.unop x_1 ⟶[V] Opposite.unop x)