have lt : i < nfa.nodes.size := Nat.lt_of_succ_lt_succ lt
case inr
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
i : ℕ
isLt : i < nfa.nodes.size + 1
lt : i.succ < nfa.nodes.size + 1
⊢ (↑(nfa.pushNode (Node.sparse c ↑next) ⋯))[i] = Node.done ↔ i = 0
case inr
c : Data.Classes
nfa : NFA
next : Fin nfa.nodes.size
h₁ : 0 < nfa.nodes.size
h₂ : ∀ (i : ℕ) (isLt : i < nfa.nodes.size), nfa[i] = Node.done ↔ i = 0
eq : nfa.pushRegex next (Data.Expr.classes c) = nfa.pushNode (Node.sparse c ↑next) ⋯
i : ℕ
isLt : i < nfa.nodes.size + 1
lt✝ : i.succ < nfa.nodes.size + 1
lt : i < nfa.nodes.size
⊢ (↑(nfa.pushNode (Node.sparse c ↑next) ⋯))[i] = Node.done ↔ i = 0