Theorem: Grammar.ExampleGrammar.productions_eq_ex_productions (FormalSystems/Chomsky/Grammar.lean)

State before:
α 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 : GenericProduction ExampleGrammar.Z ExampleGrammar.V
⊢ p ∈ ExampleGrammar.productions ↔ p ∈ ExampleProductions
Tactic:
simp [ExampleGrammar]
State after:
no goals