More canonical maps

This MR:

• Provides new implementations of gmap/gset, Pmap/Pset, Nmap/Nset and Zmap/Zset based on the "canonical" version of binary tries by Appel and Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma types and enjoy:
  • More definitional equalities, because maps are no longer equipped with a proof of canonicity. This means more equalities can be proved by reflexivity or even by conversion as part of unification. For example, {[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]} and {[ 1 ]} ∖ {[ 1 ]} = ∅ hold definitionally.
  • The use in nested recursive definitions. For example, Inductive gtest := GTest : gmap nat gtest → gtest. (The old map types would violate Coq's strict positivity condition due to the Sigma type.)
• Makes map_fold a primitive of the FinMap, and derive map_to_list from it. (Before map_fold was derived from map_to_list.) This makes it possible to use map_fold in nested-recursive definitions on maps. For example, Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts.

This MR contains a bunch of tests:

• To show that we indeed have more definitional equalities that can be proved by reflexivity.
• We can use gmap and pmap in nested recursive definitions.
• Computations with vm_compute on "big" pmap/gmaps (size >100.000), which would only terminate if the complexity is n-log-n.
• Compared to the old versions, the computations with vm_compute are slightly faster.
• Computations with reflexivity on small pmap/gmaps (size 1000), showing that the even with Coq's naive reduction computation is reasonable (<1 second).
• More tests for simpl/cbn for Pmap (and a fix akin to Opaque gmap_empty to make those work). We also should have such tests for Pset, but I leave that for a future MR.

/cc @amintimany since we were chatting about this during the PKVM meeting in Aarhus.