have inBounds := nfa.inBounds ⟨i, h⟩
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
nfa : NFA
i j : ℕ
h : i < nfa.nodes.size
mem : j ∈ nfa[i].εStep
inBounds : nfa.nodes[↑⟨i, h⟩].inBounds nfa.nodes.size
⊢ j < nfa.nodes.size