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