fact: Definition gmap_uncurry `{Countable K1, Countable K2} {A} : gmap K1 (gmap K2 A) → gmap (K1 * K2) A := map_fold (λ i1 m' macc, map_fold (λ i2 x, <[(i1,i2):=x]>) macc m') ∅.
imports: stdpp(mapset pmap) stdpp(options)