simp [result, DerivationStep.fromRule, Word.epsilon]
α nt : Type
Z : Finset α
V : Finset nt
Prod : Finset α → Finset nt → Type
inst✝ : Production α nt Prod
G : Grammar Prod
u : Word ({ x // x ∈ G.V } ⊕ { x // x ∈ G.Z })
p : { x // x ∈ G.productions }
⊢ result (fromRule p) = Production.rhs ↑p
no goals