simp
c : Char
nfa : NFA
next : Fin nfa.nodes.size
eq : nfa.pushRegex next (Data.Expr.char c) = nfa.pushNode (Node.char c ↑next) ⋯
⊢ nfa.nodes.size ≤ ↑(↑(nfa.pushNode (Node.char c ↑next) ⋯)).start
no goals