. intro assm i mem
  intro k cls
  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 ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) → ∀ i ∈ S, nfa.εClosure i ⊆ S

case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
case mpr
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, nfa.εClosure i ⊆ S) → ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S