∀ {B : Type u_2} [inst : Quiver B] {a : B}
  (motive : (x x_1 : B) → Quiver.Path a x → CategoryTheory.FreeBicategory.Hom x x_1 → Sort u_3) (x x_1 : B)
  (p : Quiver.Path a x) (f : x ⟶ x_1)
  (h_1 : (x x_2 : B) → (p : Quiver.Path a x) → (f : x ⟶ x_2) → motive x x_2 p (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (x : B) → (p : Quiver.Path a x) → motive x x p (CategoryTheory.FreeBicategory.Hom.id x))
  (h_3 :
    (x x_2 : B) →
      (p : Quiver.Path a x) →
        (b : B) →
          (f : CategoryTheory.FreeBicategory.Hom x b) →
            (g : CategoryTheory.FreeBicategory.Hom b x_2) → motive x x_2 p (f.comp g)),
  (match x, x_1, p, CategoryTheory.FreeBicategory.Hom.of f with
    | x, x_2, p, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_2 p f
    | x, .(x), p, CategoryTheory.FreeBicategory.Hom.id .(x) => h_2 x p
    | x, x_2, p, f.comp g => h_3 x x_2 p b f g) =
    h_1 x x_1 p f