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