∀ {B : Type u_2} [inst : Quiver B] {a : B} (motive : (x : B) → Quiver.Path a x → Sort u_3)
  (h_1 : Unit → motive a Quiver.Path.nil) (h_2 : (x b : B) → (p : Quiver.Path a b) → (f : b ⟶ x) → motive x (p.cons f)),
  (match a, Quiver.Path.nil with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_1 ()