simp [DFA.del_star_curried, Option.bind_eq_bind, TotalDFA.del_star']
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ DFA.del_star_curried M (head✝ :: xs) q =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝ :: xs))
α qs : Type
M : DFA α qs
head✝ : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
ih :
  ∀ {q : { x // x ∈ M.Q }},
    DFA.del_star_curried M xs q = ↑(TotalDFA.del_star' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, xs))
q : { x // x ∈ M.Q }
⊢ Option.bind (M.δ (q, head✝)) (DFA.del_star_curried M xs) =
    ↑(TotalDFA.del_star' (DFA.toTotalDFA M)
        (TotalDFA.δ' (DFA.toTotalDFA M) ({ val := some q, property := ⋯ }, head✝), xs))