have inBounds := nfa.inBounds i
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
⊢ nfa[i].inBounds nfa.nodes.size
n : Node
nfa : NFA
i : Fin nfa.nodes.size
hn : nfa[i] = n
inBounds : nfa.nodes[↑i].inBounds nfa.nodes.size
⊢ nfa[i].inBounds nfa.nodes.size