∀ {B : Type u} [inst : Quiver B] {a : B} (x x_1 : B) (x_2 : Quiver.Path a x) (f : x ⟶ x_1),
  CategoryTheory.FreeBicategory.normalizeIso x_2 (CategoryTheory.FreeBicategory.Hom.of f) =
    CategoryTheory.Iso.refl
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := x_2 })
        (CategoryTheory.FreeBicategory.Hom.of f))