simp at h₂
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
i j : ℕ
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next Data.Expr.empty = nfa.pushNode Node.fail ⋯
h₂✝ : i < (↑(nfa.pushNode Node.fail ⋯)).nodes.size
step : (∃ c, j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].charStep c) ∨ j ∈ (↑(nfa.pushNode Node.fail ⋯))[i].εStep
h₂ : i < nfa.nodes.size + 1
⊢ j = ↑next ∨ nfa.nodes.size ≤ j