intro eq
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
⊢ result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯ → (↑result)[i] = nfa[i]
i : ℕ
a✝ : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next (Data.Expr.classes a✝) = result
h : i < nfa.nodes.size
eq : result = nfa.pushNode (Node.sparse a✝ ↑next) ⋯
⊢ (↑result)[i] = nfa[i]