intro eqv₁ eqv₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
⊢ s₁ ≈ s₂ → t₁ ≈ t₂ → s₁ ++ t₁ ≈ s₂ ++ t₂
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ t₁ t₂ : FormalSum R X
eqv₁ : s₁ ≈ s₂
eqv₂ : t₁ ≈ t₂
⊢ s₁ ++ t₁ ≈ s₂ ++ t₂