∀ {β : Type u_1} [inst : Fintype β] (L : SummationFilter β) [inst_1 : DecidablePred fun x => x ∈ L.support]
  (s : Finset β), (∀ i ∈ L.support, i ∈ s) → (∀ i ∉ L.support, i ∉ s) → s = L.support.toFinset