∀ {B : Type u} [inst : Quiver B] {a b c : B} {f g h : CategoryTheory.FreeBicategory.Hom a b}
  (i : CategoryTheory.FreeBicategory.Hom b c) (η : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right i (η.vcomp θ))
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_right i η).vcomp
      (CategoryTheory.FreeBicategory.Hom₂.whisker_right i θ))