simp [NFA.done] at isLt
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i < done.nodes.size
⊢ i = 0
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i✝ : Fin nfa.nodes.size
i : ℕ
isLt : i = 0
⊢ i = 0