simp at h
nfa : NFA
c : Char
pos : String.Pos
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
target : Fin nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
c'✝ : Char
target'✝ : ℕ
heq✝ : nfa[target] = Node.char c'✝ target'✝
h✝ : c = c'✝
h :
  (let_fun isLt := ⋯;
    let currentSave := saveSlots.get ↑target ⋯;
    exploreεClosure nfa pos next currentSave none saveSlots ⟨target'✝, isLt⟩ #[]) =
    (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'
nfa : NFA
c : Char
pos : String.Pos
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
target : Fin nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
c'✝ : Char
target'✝ : ℕ
heq✝ : nfa[target] = Node.char c'✝ target'✝
h✝ : c = c'✝
h :
  exploreεClosure nfa pos next (saveSlots.get ↑target ⋯) none saveSlots ⟨target'✝, ⋯⟩ #[] =
    (matched', next', saveSlots')
⊢ ∀ (i j : Fin nfa.nodes.size), i ∈ next' → ↑j ∈ nfa.εStep ↑i → j ∈ next'