let (matched', init', saveSlots) := init
nfa : NFA
it : String.Iterator
saveSize : ℕ
matched : Option (Array (Option String.Pos))
v : it.Valid
hsome : matched.isSome = true
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots nfa.start #[] = init
h : captureNext.go nfa saveSize it init.2.1 SparseSet.empty init.2.2 init.1 = matched
⊢ ∃ 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))
v : it.Valid
hsome : matched.isSome = true
saveSlots✝ : Vec (Array (Option String.Pos)) nfa.nodes.size
_hs : (Vec.ofFn fun x => captureNext.initSave saveSize) = saveSlots✝
init : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
init' : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.i SparseSet.empty (captureNext.initSave saveSize) none saveSlots✝ nfa.start #[] =
    (matched', init', saveSlots)
h :
  captureNext.go nfa saveSize it (matched', init', saveSlots).2.1 SparseSet.empty (matched', init', saveSlots).2.2
      (matched', init', saveSlots).1 =
    matched
⊢ ∃ 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