. intro assm i mem _ j step
  apply Set.mem_of_mem_of_subset _ (assm i mem)
  exact εClosure.step (εStep_of_εStep step) .base
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
no goals