induction cls with
| base => exact mem
| @step i j k step _ ih =>
  cases Nat.decLt i nfa.nodes.size with
  | isTrue lt =>
    simp [εStep, lt] at step
    exact ih (assm i mem lt j step)
  | isFalse nlt => simp [εStep, nlt] at step
case mp
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
i : ℕ
mem : i ∈ S
k : ℕ
cls : k ∈ nfa.εClosure i
⊢ k ∈ S
no goals