∀ {V : Type u_1} [inst : Quiver V] (v w : V) (motive : Quiver.Path.BoundedPaths v w 0 → Prop)
  (x : Quiver.Path.BoundedPaths v w 0), (∀ (q : Quiver.Path v w) (hq : q.length ≤ 0), motive ⟨q, hq⟩) → motive x