simp [pushNode, get_eq_nodes_get]
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.pushNode node inBounds).val[i] = nfa[i]
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h : i < nfa.nodes.size
⊢ (nfa.nodes.push node)[i] = nfa.nodes[i]