let S := { j | ∃ isLt : j < nfa.nodes.size, ⟨j, isLt⟩ ∈ next }
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next