{B : Type u_1} →
  [inst : Quiver B] →
    (motive : (x x_1 : CategoryTheory.FreeBicategory B) → (x ⟶ x_1) → Sort u_3) →
      (x x_1 : CategoryTheory.FreeBicategory B) →
        (x_2 : x ⟶ x_1) →
          ((x x_3 : B) → (f : x ⟶ x_3) → motive x x_3 (CategoryTheory.FreeBicategory.Hom.of f)) →
            ((a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a)) →
              ((x x_3 b : B) →
                  (f : CategoryTheory.FreeBicategory.Hom x b) →
                    (g : CategoryTheory.FreeBicategory.Hom b x_3) → motive x x_3 (f.comp g)) →
                motive x x_1 x_2