proposition: Lemma lookup_gmap_curry (m : gmap (K1 * K2) A) i j : gmap_curry m !! i ≫= (.!! j) = m !! (i, j).
proof: Proof. apply (map_fold_ind (λ mr m, mr !! i ≫= (.!! j) = m !! (i, j))). { by rewrite !lookup_empty. } clear m; intros [i' j'] x m12 mr Hij' IH. destruct (decide (i = i')) as [->|]. - rewrite lookup_partial_alter. destruct (decide (j = j')) as [->|]. + destruct (mr !! i'); simpl; by rewrite !lookup_insert. + destruct (mr !! i'); simpl; by rewrite !lookup_insert_ne by congruence. - by rewrite lookup_partial_alter_ne, lookup_insert_ne by congruence. Qed.
imports: stdpp(mapset pmap) stdpp(options)