generalize h' : cs ++ [c] = cs' at h
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
h : nfa.stepIn start i j (cs ++ [c])
⊢ cs = []
nfa : NFA
i j : ℕ
cs : List Char
c : Char
start : ℕ
cs' : List Char
h' : cs ++ [c] = cs'
h : nfa.stepIn start i j cs'
⊢ cs = []