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