apply RegularGrammar.RegularDerivation.fromDerivation
case h.d
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ RegularGrammar.RegularDerivation (toGrammar M) M.q₀ a✝
case h.d.derivation
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Grammar.Derivation (toGrammar M) [Sum.inl M.q₀] ?h.d.w'

case h.d.h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Sum.inr <$> a✝ = ?h.d.w'

case h.d.w'
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ (toGrammar M).Z }
h : a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
d : Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
⊢ Word ({ x // x ∈ (toGrammar M).V } ⊕ { x // x ∈ (toGrammar M).Z })