{α : Type u} →
  {σ : Type v} →
    {M : NFA α σ} →
      {motive : (a a_1 : σ) → (a_2 : List α) → M.Path a a_1 a_2 → Sort u_1} →
        {a a_1 : σ} →
          {a_2 : List α} →
            (t : M.Path a a_1 a_2) →
              ((s : σ) → motive s s [] (NFA.Path.nil s)) →
                ((t s u : σ) →
                    (a : α) →
                      (x : List α) →
                        (a_3 : t ∈ M.step s a) →
                          (a_4 : M.Path t u x) → motive s u (a :: x) (NFA.Path.cons t s u a x a_3 a_4)) →
                  motive a a_1 a_2 t