simp [h, this]
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' : ℕ
hn : nfa[↑target] = Node.char c' target'
hc : ¬c = c'
this : ∀ (i : ℕ), i ∉ nfa.charStep (↑target) c
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ ∀ (j : Fin nfa.nodes.size), j ∈ next' ↔ j ∈ next ∨ ∃ i ∈ nfa.charStep (↑target) c, ↑j ∈ nfa.εClosure i
no goals