∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] {𝒜 : Finset (Finset α)} {a : α}
  {f : Finset α → β} {s t u : Finset α}, a ∉ s → t ∈ 𝒜 → u ∈ 𝒜 → t = s → u = insert a s → collapse✝ 𝒜 a f s = f t + f u