Library Coq.Sets.Uniset
Sets as characteristic functions
uniset inclusion
uniset equality
uniset union
All the proofs that follow duplicate Multiset_of_A
Here we should make uniset an abstract datatype, by hiding Charac,
union, charac; all further properties are proved abstractly
specific for treesort