simp at this
case charStep.cons
nfa : NFA
i j : ℕ
c : Char
start : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step✝ : j ∈ nfa[i].charStep c✝
head✝ : Char
tail✝ : List Char
h' : head✝ :: tail✝ ++ [c] = [c✝]
this : (head✝ :: tail✝ ++ [c]).length = [c✝].length
⊢ head✝ :: tail✝ = []
no goals