apply Iff.intro
nfa : NFA
S : Set ℕ
⊢ (∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S) ↔ ∀ i ∈ S, nfa.εClosure i ⊆ S
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