unfold AcceptedLanguage
α qs : Type
M : DFA α qs
⊢ AcceptedLanguage M = NFA.AcceptedLanguage (toNFA M)
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = NFA.AcceptedLanguage (toNFA M)