. intro h; rw [h]; exact ⟨ rfl, rfl ⟩
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 mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
⊢ p₁.lhs = p₂.lhs ∧ p₁.rhs = p₂.rhs → p₁ = p₂