∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : CategoryTheory.Bicategory.Adj B),
  CategoryTheory.Bicategory.Adj.forget₁.mapId x = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id x).l