intro h
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁ = p₂ → p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs
case mp
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h : p₁ = p₂
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs