intro s₁ s₂ neqv
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (a b : FormalSum R X),
    beq_quot (Quotient.mk (formalSumSetoid R X) a) (Quotient.mk (formalSumSetoid R X) b) = false →
      ¬Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
neqv : beq_quot (Quotient.mk (formalSumSetoid R X) s₁) (Quotient.mk (formalSumSetoid R X) s₂) = false
⊢ ¬Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂