apply pushNode_get_lt i h
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h : i < nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.classes a✝) = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑(nfa.pushNode (Node.sparse a✝ ↑next) ⋯))[i] = nfa[i]
no goals