∀ {V : Type u_1} [inst : Quiver V] (r : V) (height : V → ℕ),
  (∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b) →
    (∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)) → ∀ (b : V), Nonempty (Quiver.Path r b)