proposition: Lemma gmap_curry_uncurry_non_empty (m : gmap K1 (gmap K2 A)) : (∀ i x, m !! i = Some x → x ≠ ∅) → gmap_curry (gmap_uncurry m) = m.
proof: Proof. intros Hne. apply map_eq; intros i. destruct (m !! i) as [m2|] eqn:Hm. - destruct (gmap_curry (gmap_uncurry m) !! i) as [m2'|] eqn:Hcurry. + f_equal. apply map_eq. intros j. trans (gmap_curry (gmap_uncurry m) !! i ≫= (.!! j)). { by rewrite Hcurry. } by rewrite lookup_gmap_curry, lookup_gmap_uncurry, Hm. + rewrite lookup_gmap_curry_None in Hcurry. exfalso; apply (Hne i m2), map_eq; [done|intros j]. by rewrite lookup_empty, <-(Hcurry j), lookup_gmap_uncurry, Hm. - apply lookup_gmap_curry_None; intros j. by rewrite lookup_gmap_uncurry, Hm. Qed.
imports: stdpp(mapset pmap) stdpp(options)