∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : AddCommMonoid β] [inst_1 : DecidableEq α],
  a ∉ s →
    ∀ (f : Finset α → β), ∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)