simp [pushRegex, Node.charStep, hmem]
case sparse
r : Data.Expr
cs : List Char
cls : Data.Classes
c : Char
hmem : c ∈ cls
nfa : NFA
next : Fin nfa.nodes.size
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq : nfa.pushRegex next (Data.Expr.classes cls) = nfa'
this : nfa.nodes.size ≤ ↑(↑nfa').start
⊢ ↑next ∈
    (↑(nfa.pushRegex next (Data.Expr.classes cls)))[↑(↑(nfa.pushRegex next (Data.Expr.classes cls))).start].charStep c
no goals