have : nfa.nodes.size ≤ nfa'.val.start.val := ge_pushRegex_start eq
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'
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]
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
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start [c]