rw [← append_coords]
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t) ++ scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀
case cons.h
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
h : R × X
t : List (R × X)
ih : scmul a t ++ scmul b t ≈ scmul (a + b) t
x₀ : X
il₁ : coords (scmul a t ++ scmul b t) x₀ = coords (scmul (a + b) t) x₀ := congrFun ih x₀
⊢ coords (scmul a (h :: t)) x₀ + coords (scmul b (h :: t)) x₀ = coords (scmul (a + b) (h :: t)) x₀