Proofs of extensionality for sets and maps

Prove extensionality for our representations of finite sets and maps as sorted lists.

Remark: There is a bit of redundancy that could be avoided if we defined sets as maps to unit instead of defining maps as sets of pairs sorted using a partial ordering.

We should also move generic lemmas about List.Forall and sorting out of the set module or even replace these two modules by some predefined implementation of finite sets and maps in Coq.