Library Coq.FSets.FSetFacts
This functor derives additional facts from FSetInterface.S. These
facts are mainly the specifications of FSetInterface.S written using
different styles: equivalence and boolean equalities.
Moreover, we prove that E.Eq and Equal are setoid equalities.
First, a functor for Weak Sets in functorial version.
Specifications written using equivalences
Useful tactic for simplifying expressions like In y (add x (union s s'))
Specifications written using boolean predicates
E.eq and Equal are setoid equalities
Now comes variants for self-contained weak sets and for full sets.
For these variants, only one argument is necessary. Thanks to
the subtyping WS<=S, the Facts functor which is meant to be
used on modules (M:S) can simply be an alias of WFacts.