∀ {ι : Type u_2} {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (f : ι → M) (a : ι) (s : List ι),
  a ∉ s.toFinset → f a + ∑ m ∈ s.toFinset, List.count m s • f m = f a + ∑ x ∈ s.toFinset, List.count x (a :: s) • f x