rfl
α nt : Type
G : RegularGrammar α nt
p✝ : { x // x ∈ G.productions }
Z : Finset α
V : Finset nt
p : RegularProduction Z V
lhs✝ : { x // x ∈ V }
h : isEps (eps lhs✝)
⊢ eps lhs✝ = eps (lhs (eps lhs✝))
no goals