{V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] →
      [G.LocallyFinite] →
        (v : V) →
          (n : ℕ) → Nat.below (motive := fun n => (u : V) → Finset (G.Walk u v)) n → (u : V) → Finset (G.Walk u v)