exact eq
case intro.intro.intro.intro.intro.inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
next' i : ℕ
cs : List Char
eq✝ : nfa.pushRegex next r = result
assm : next' < nfa.nodes.size
i' : ℕ
pcs scs : List Char
left✝ : cs = pcs ++ scs
path : (↑result).pathIn nfa.nodes.size i i' pcs
step : (↑result).stepIn nfa.nodes.size i' next' scs
eq : next' = ↑next
⊢ next' = ↑next
no goals