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