∀ {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  {a b c : CategoryTheory.EnrichedCat V} (f : CategoryTheory.EnrichedFunctor V ↑a ↑b)
  (g : CategoryTheory.EnrichedFunctor V ↑b ↑c),
  CategoryTheory.EnrichedCat.whiskerRight (CategoryTheory.CategoryStruct.id f) g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedFunctor.comp V f g)