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

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