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