Additions to the powerset module

[rahulc29]

I believe the following additions could be made to the Powerset module :

1. [x] A ∈ₚ operator that produces an hProp for x ∈ₚ A rather than a general type
2. [x] Binary unions and intersections
3. [x] Indexed unions and intersections
4. [x] A separate type for "inhabited subsets"
5. [x] The complement of a subset

While these are easy to define I found consistently needing these and believe others could benefit from it too.

I'd be happy to drop in a PR.