simp
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k ([] ++ [c])
case base
j k : ℕ
nfa : NFA
i : ℕ
cs : List Char
c : Char
start i✝ : ℕ
h : start ≤ i✝
assm : i✝ < nfa.nodes.size
step : k ∈ nfa[i✝].charStep c
⊢ nfa.pathIn (min start k) i✝ k [c]