apply ih
α qs : Type
M : TotalDFA α qs
head✝ : { x // x ∈ M.Z }
tail✝ : List { x // x ∈ M.Z }
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 }
⊢ some (δ' M (q, head✝)) >>= DFA.del_star_curried M.toDFA tail✝ = some (del_star' M (q, head✝ :: tail✝))
no goals