exact .inl (And.right step)
i j : ℕ
r : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : nfa.nodes.size ≤ i
eq : nfa.pushRegex next (Data.Expr.classes r) = nfa.pushNode (Node.sparse r ↑next) ⋯
h₂✝ : i < (↑(nfa.pushNode (Node.sparse r ↑next) ⋯)).nodes.size
h₂ : i < nfa.nodes.size + 1
this : i = nfa.nodes.size
step : (∃ x, x ∈ r) ∧ j = ↑next
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
no goals