simp_rw [h, del_star_curried, NFA.Run.last]
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
h : w = ε
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.final q h))
no goals