Library Coq.Sets.Ensembles
NB: The following definition builds-in equality of elements in U as
Leibniz equality.
This may have to be changed if we replace U by a Setoid on U
with its own equality eqs, with
In_singleton: (y: U)(eqs x y) -> (In (Singleton x) y).
Extensionality Axiom