exact εClosure.step (εStep_of_εStep step) .base
nfa : NFA
S : Set ℕ
assm : ∀ i ∈ S, nfa.εClosure i ⊆ S
i : ℕ
mem : i ∈ S
x✝ : i < nfa.nodes.size
j : ℕ
step : j ∈ nfa[i].εStep
⊢ j ∈ nfa.εClosure i
no goals