simp [DerivationStep.fromRule, DerivationStep.result, h]
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ DerivationStep.result (DerivationStep.fromRule p) = ε
α nt : Type
G : RegularGrammar α nt
p : { x // x ∈ G.productions }
v : { x // x ∈ G.V }
h : ↑p = eps v
⊢ Production.rhs (eps v) = ε