apply Quotient.ind₂ (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = true → x₁ = x₂)
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
⊢ ∀ (x₁ x₂ : R[X]), beq_quot x₁ x₂ = true → x₁ = x₂
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) = true →
      Quotient.mk (formalSumSetoid R X) a = Quotient.mk (formalSumSetoid R X) b