match p₁ with
| ⟨ l, r, _ ⟩ => simp at h₁; simp at h₂; simp_rw [h₁, h₂]
case mpr
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
h₁ : p₁.lhs = p₂.lhs
h₂ : p₁.rhs = p₂.rhs
⊢ p₁ = p₂
no goals