simp [scmul]
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ scmul a [] ++ scmul b [] ≈ scmul (a + b) []
case nil
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
a b : R
⊢ [] ≈ []