proposition: Lemma lookup_gmap_uncurry (m : gmap K1 (gmap K2 A)) i j : gmap_uncurry 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' m2 m m12 Hi' IH. apply (map_fold_ind (λ m2r m2, m2r !! (i,j) = <[i':=m2]> m !! i ≫= (.!! j))). { rewrite IH. destruct (decide (i' = i)) as [->|]. - rewrite lookup_insert, Hi'; simpl; by rewrite lookup_empty. - by rewrite lookup_insert_ne by done. } intros j' y m2' m12' Hj' IH'. destruct (decide (i = i')) as [->|]. - rewrite lookup_insert; simpl. destruct (decide (j = j')) as [->|]. + by rewrite !lookup_insert. + by rewrite !lookup_insert_ne, IH', lookup_insert by congruence. - by rewrite !lookup_insert_ne, IH', lookup_insert_ne by congruence. Qed.
imports: stdpp(mapset pmap) stdpp(options)