induction h with
| nil cls => simp [pathIn_iff_εClosure.mpr cls]
| @snoc i j k c m _ step cls ih =>
  simp [charStep] at step
  have ih' : nfa.pathIn (min 0 j) nfa.start j (m ++ [c]) :=
    ih.snoc_char i.isLt step
  simp at ih'
  have := ih'.trans (pathIn_iff_εClosure.mpr cls)
  simp at this
  exact this
nfa : NFA
i : Fin nfa.nodes.size
m : List Char
h : nfa.reaches i m
⊢ nfa.pathIn 0 (↑nfa.start) (↑i) m
no goals