∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.snd B C).mapId x).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2)