simp at h₂
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ }.rhs = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂
α nt : Type
Z : Finset α
V : Finset nt
p₁ p₂ : GenericProduction Z V
l r : Word ({ x // x ∈ V } ⊕ { x // x ∈ Z })
lhs_contains_var✝ : ∃ v, Sum.inl v ∈ l
h₁ : l = p₂.lhs
h₂ : r = p₂.rhs
⊢ { lhs := l, rhs := r, lhs_contains_var := lhs_contains_var✝ } = p₂