apply toGrammar_lang_subs_lang
case h.mp
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)