cases step with
| charStep h₁ h₂ step => exact eqs ▸ path.snoc_char h₂ step
| εStep h₁ h₂ step => simp [eqs, path.snoc_ε h₂ step]
case intro.intro.intro.intro.intro
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathIn (min start next) i next cs
no goals