∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b c : B) {X Y : a ⟶ b} (η : X ⟶ Y) (x : b ⟶ c),
  ((CategoryTheory.Bicategory.precomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerRight η x