∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  (x : CategoryTheory.FreeBicategory B),
  (CategoryTheory.FreeBicategory.lift F).mapId x =
    CategoryTheory.Iso.refl (CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id x))