cases cs with
| nil => rfl
| cons _ _ =>
  have := congrArg List.length h'
  simp at this
case charStep
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
h' : cs ++ [c] = [c✝]
⊢ cs = []
no goals