induction path with
| base _ => exact .base
| @step i j k cs cs' step _ ih =>
  simp at h
  simp [h] at *
  cases step with
  | εStep _ _ step =>
    exact εClosure.step (εStep_of_εStep step) ih
i i' : ℕ
nfa : NFA
start : ℕ
cs : List Char
h : [] = cs
path : nfa.pathIn start i i' cs
⊢ i' ∈ nfa.εClosure i
no goals