unfold captureNext at h
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
h : captureNext nfa it saveSize = matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
h :
  (let saveSlots := Vec.ofFn fun x => captureNext.initSave saveSize;
    match exploreεClosure nfa it.pos SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] with
    | (matched, init, saveSlots) => captureNext.go nfa saveSize it init SparseSet.empty saveSlots matched) =
    matched
v : it.Valid
hsome : matched.isSome = true
⊢ ∃ s l m r,
    Substring.ValidFor l m r s ∧ it.toString = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done