∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] (n : ℕ) [inst_2 : DecidableEq α],
  Set.powersetCard.subAddAction G α n = { carrier := Set.powersetCard α n, vadd_mem' := ⋯ }