apply pushRegex.empty eq
case empty
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ Expr.matches cs Expr.empty
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq : nfa.pushRegex next Expr.empty = result
path : (↑result).pathToNext (↑next) nfa.nodes.size (↑(↑result).start) cs
⊢ result = nfa.pushNode Node.fail ⋯ → Expr.matches cs Expr.empty