have := le_of_pathIn_left rest
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝ this h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
⊢ Expr.matches cs Expr.epsilon
case intro.intro.intro.intro.intro.εStep.step.εStep
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next Expr.epsilon = result
eq : result = nfa.pushNode (Node.epsilon ↑next) ⋯
i : ℕ
h₂✝¹ : i < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
this✝¹ this✝ h₁✝¹ step✝ : True
j✝ : ℕ
cs₂✝ : List Char
rest : (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).pathIn nfa.nodes.size j✝ nfa.nodes.size cs₂✝
h₁✝ : nfa.nodes.size ≤ nfa.nodes.size
h₂✝ : nfa.nodes.size < (↑(nfa.pushNode (Node.epsilon ↑next) ⋯)).nodes.size
eqs : cs = [] ++ cs₂✝
step : j✝ = ↑next
this : nfa.nodes.size ≤ j✝
⊢ Expr.matches cs Expr.epsilon