filter the powerset

Stream: general

[Peter Nelson]

For S: finset \alpha, I have a proposition P defined over the subsets of S by

P (X : finset \alpha) (hX : X \ss S)

I would like to filter the power set of S by P to construct the set {X \in powerset X | P X (sorry)}. However, I don't know how to fill in the sorry. My functional programming is shaky, but I can't see a way to get an hX from the left to the right of the 'such that' in the set definition, although it seems that a proof should 'obviously' exist. Can someone help me with this?

[Floris van Doorn]

Try {X : finset α | ∃ (hX : X ⊆ S), P X hX}