rfl
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
hyp : ∀ (x : X), coords [] x = coords s₂ x
x : X
h : coords [] x = coords s₂ x := hyp x
⊢ coords [] x = 0
no goals