simp [coords, step]
case cons
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
s₁✝ s₂✝ : FormalSum R X
a : R
x : X
s₁ s₂ : FormalSum R X
a✝ : ElementaryMove R X s₁ s₂
step : coords s₁ x₀ = coords s₂ x₀
⊢ coords ((a, x) :: s₁) x₀ = coords ((a, x) :: s₂) x₀
no goals