have h (i : Nat) (isLt : i < NFA.done.nodes.size) : done[i] = Node.done ↔ i = 0 := by
  simp [NFA.done] at *
  suffices i = 0 by
    subst this
    simp
    rfl
  simp [NFA.done] at isLt
  match i with
  | 0 => rfl
  | i + 1 => contradiction
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
⊢ nfa[i] = Node.done ↔ ↑i = 0
r : Data.Expr
nfa : NFA
eq : compile r = nfa
i : Fin nfa.nodes.size
h : ∀ (i : ℕ) (isLt : i < done.nodes.size), done[i] = Node.done ↔ i = 0
⊢ nfa[i] = Node.done ↔ ↑i = 0