∀ {α : Type u_1} {σ : Type u_2} {M : NFA α σ} (motive : (x : List α) → (t s : σ) → Nonempty (M.Path s t x) → Prop)
  (x : List α) (t s : σ) (p : Nonempty (M.Path s t x)),
  (∀ (s : σ), motive [] s s ⋯) →
    (∀ (t s s' : σ) (a : α) (x : List α) (h₁ : s' ∈ M.step s a) (h₂ : M.Path s' t x), motive (a :: x) t s ⋯) →
      motive x t s p