Initial version of a finset theory over a choiceType.

This works by quotienting uniq lists with the equality up-to-
permutation.

Currently, all basic operators (empty, full, union, intersection,
complement) with basic algebra properties are defined/proved. Some
operators require the base type to be a finType (full, complement).

The cardinal is also defined, but the related theory has yet to be
derived.

Nothing is said about \subset, \proper.