exact eqs ▸ path.snoc_char h₂ step
case intro.intro.intro.intro.intro.charStep
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs : List Char
path : nfa.pathIn start i i' pcs
c✝ : Char
h₁ : start ≤ i'
h₂ : i' < nfa.nodes.size
step : next ∈ nfa[i'].charStep c✝
eqs : cs = pcs ++ [c✝]
⊢ nfa.pathIn (min start next) i next cs
no goals