apply RegularDerivation.fromDerivation
case h.right.h.d
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ RegularDerivation G G.start w
case h.right.h.d.derivation
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Grammar.Derivation G [Sum.inl G.start] ?h.right.h.d.w'

case h.right.h.d.h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Sum.inr <$> w = ?h.right.h.d.w'

case h.right.h.d.w'
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ G.Z }
d : Grammar.Derivation G [Sum.inl G.start] (Sum.inr <$> w)
⊢ Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })