FSetAVL : Implementation of FSetInterface via AVL trees

This module implements finite sets using AVL trees. It follows the implementation from Ocaml's standard library, All operations given here expect and produce well-balanced trees (in the ocaml sense: heights of subtrees shouldn't differ by more than 2), and hence has low complexities (e.g. add is logarithmic in the size of the set). But proving these balancing preservations is in fact not necessary for ensuring correct operational behavior and hence fulfilling the FSet interface. As a consequence, balancing results are not part of this file anymore, they can now be found in FSetFullAVL. Four operations (union, subset, compare and equal) have been slightly adapted in order to have only structural recursive calls. The precise ocaml versions of these operations have also been formalized (thanks to Function+measure), see ocaml_union, ocaml_subset, ocaml_compare and ocaml_equal in FSetFullAVL. The structural variants compute faster in Coq, whereas the other variants produce nicer and/or (slightly) faster code after extraction.

This is just a compatibility layer, the real implementation is now in MSetAVL