∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D),
  (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor