have w_cast : w = w' := rfl
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
case h
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
⊢ (∃ qf ∈ DFA.del_star M (M.q₀, w), qf ∈ M.F) ↔ w ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA