Simplify usage of set and map modules
Because they rely on the section mechanism, using a function or a lemma from the set and map modules typically requires to provide some function and lemmas from the comparable module. This could be avoided in several ways:
- by defining wrapper modules that specialize sets and maps with comparable data in the sense of the comparable module
- by replacing the sections by type classes and registering an instance for comparable data in the sense of the comparable module.