let ceq := coords_well_defined x ((a₀, x₀) :: t) t eq₁
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
⊢ coords t x = coords s₂ x
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
s₁ s₂ : FormalSum R X
h : R × X
t : List (R × X)
a₀ : R
x₀ : X
hyp : ∀ (x : X), coords ((a₀, x₀) :: t) x = coords s₂ x
p : 0 = a₀
eq₁ : (a₀, x₀) :: t ≃ t
x✝ : List.length t < List.length (h :: t)
x : X
ceq : coords ((a₀, x₀) :: t) x = coords t x := coords_well_defined x ((a₀, x₀) :: t) t eq₁
⊢ coords t x = coords s₂ x