induction w generalizing q
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
⊢ DFA.del_star_curried M.toDFA w q = some (del_star' M (q, w))
case nil
α qs : Type
M : TotalDFA α qs
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA [] q = some (del_star' M (q, []))

case cons
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
tail_ih✝ : ∀ {q : { x // x ∈ M.Q }}, DFA.del_star_curried M.toDFA tail✝ q = some (del_star' M (q, tail✝))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M.toDFA (head✝ :: tail✝) q = some (del_star' M (q, head✝ :: tail✝))