proposition: Lemma gmap_curry_non_empty (m : gmap (K1 * K2) A) i x : gmap_curry m !! i = Some x → x ≠ ∅.
proof: Proof. intros Hm ->. eapply eq_None_not_Some; [|by eexists]. eapply lookup_gmap_curry_None; intros j. by rewrite <-lookup_gmap_curry, Hm. Qed.
imports: stdpp(mapset pmap) stdpp(options)