∀ {α : Type u_2} {β : Type u_1} [inst : AddCommGroup α] {f : β → α} (e : Set α)
  (motive : (∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e) → Prop)
  (x : ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e),
  (∀ (s : Finset β) (hs : ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e), motive ⋯) → motive x