intro w ⟨_, hr⟩
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ DFA.AcceptedLanguage (DFA.fromNFA M) ⊆ AcceptedLanguage M
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
⊢ w ∈ AcceptedLanguage M