induction m using List.list_reverse_induction generalizing i with
| base => exact .nil (pathIn_iff_εClosure.mp h)
| ind m c ih =>
  have ⟨j, k, path, step, cls⟩ := pathIn.of_snoc_char h
  let j' : Fin nfa.nodes.size := ⟨j, path.lt_right nfa.start.isLt⟩
  have prev := ih (i := j') path
  exact .snoc prev step cls
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.pathIn 0 (↑nfa.start) (↑i) m
⊢ nfa.reaches i m
no goals