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