proposition: Lemma gmap_uncurry_curry (m : gmap (K1 * K2) A) : gmap_uncurry (gmap_curry m) = m.
proof: Proof. apply map_eq; intros [i j]. by rewrite lookup_gmap_uncurry, lookup_gmap_curry. Qed.
imports: stdpp(mapset pmap) stdpp(options)