refine ⟨nfa'.val.start, [], [], rfl, .base this, .εStep this nfa'.val.start.isLt ?_⟩
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
⊢ (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
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')[↑(↑nfa').start].εStep