∀ (B : Type u_2) [inst : CategoryTheory.Bicategory B] (x : B),
  (CategoryTheory.LaxFunctor.id B).map (CategoryTheory.CategoryStruct.id x) =
    (CategoryTheory.LaxFunctor.id B).map (CategoryTheory.CategoryStruct.id x)