cases h with
| εStep => simp at h'
| charStep =>
  cases cs with
  | nil => rfl
  | cons _ _ =>
    have := congrArg List.length h'
    simp at this
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 = []
no goals