∀ {V : Type u_2} [inst : Quiver V] {b : V} (motive : (x : V) → Quiver.Path b x → Prop) (x : V) (x_1 : Quiver.Path b x),
  (∀ (a : Unit), motive b Quiver.Path.nil) →
    (∀ (x d : V) (q : Quiver.Path b d) (a : d ⟶ x), motive x (q.cons a)) → motive x x_1