exact eqs ▸ .epsilon
case intro.intro.intro.intro.intro.εStep.base
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
h✝ : nfa.nodes.size ≤ nfa.nodes.size
eqs : cs = []
⊢ Expr.matches cs Expr.epsilon
no goals