cases r
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ (toNFA M).Q }
r : NFA.Run (toNFA M) q w
⊢ del_star_curried M w q = some (NFA.Run.last r)
case final
α 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✝))

case step
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q q₂✝ : { x // x ∈ (toNFA M).Q }
a✝ : { x // x ∈ (toNFA M).Z }
w✝ : Word { x // x ∈ (toNFA M).Z }
r✝ : NFA.Run (toNFA M) q₂✝ w✝
x✝ : q₂✝ ∈ (toNFA M).δ (q, a✝)
h✝ : w = a✝ :: w✝
⊢ del_star_curried M w q = some (NFA.Run.last (NFA.Run.step q x✝ r✝ h✝))