apply Set.ext
α qs : Type
M : DFA α qs
⊢ DFA.AcceptedLanguage M = DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA
case h
α qs : Type
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ M.Z }), x ∈ DFA.AcceptedLanguage M ↔ x ∈ DFA.AcceptedLanguage (DFA.toTotalDFA M).toDFA