cases Nat.lt_or_eq_of_le (Nat.le_of_succ_le_succ h) with
| inl lt => simp [lt, pushNode_get_lt _ lt]
| inr eq => simp [eq]
nfa : NFA
node : Node
inBounds : node.inBounds (nfa.nodes.size + 1)
i : Nat
h✝ : i < (nfa.pushNode node inBounds).val.nodes.size
h : i < nfa.nodes.size + 1
⊢ (nfa.pushNode node inBounds).val[i] = if h' : i < nfa.nodes.size then nfa[i] else node
no goals