simp [coeffInclusion] at hyp
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : coeffInclusion x₀ a₀ = coeffInclusion x₀ a₁
⊢ a₀ = a₁
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
x₀ : X
a₀ a₁ : R
hyp : [(a₀, x₀)] ≈ [(a₁, x₀)]
⊢ a₀ = a₁