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