unfold del_star_curried
α 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✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ del_star_curried M (a✝ :: w✝) q = some (NFA.Run.last r')
α 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✝
incl : q₂✝ ∈ (toNFA M).δ (q, a✝)
w_cast : w = a✝ :: w✝
⊢ M.δ (q, a✝) >>= del_star_curried M w✝ = some (NFA.Run.last r')