exact ⟨s, l, m, r, sv, eqs, ma⟩
re : Data.Expr
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
eq : compile re = nfa
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
eqs : it.toString = { data := l ++ m ++ r }
i : Fin nfa.nodes.size
hr : nfa.reaches i m
hdone : nfa[i] = Node.done
ma : Data.Expr.matches m re
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ Data.Expr.matches m re
no goals