∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.hom h) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.inv h) k) h_1) =
    h_1