∀ {ι : Type u_5} {α : ι → Type u_6} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → Neg (α i)] (s : (i : ι) → Finset (α i)), (Fintype.piFinset fun i => -s i) = -Fintype.piFinset s