∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans X Y)
  (θ : CategoryTheory.Lax.StrongTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = η.toLax.vCompApp θ.toLax a