proposition: Lemma map_to_list_gset_to_gmap {A} (X : gset K) (x : A) : map_to_list (gset_to_gmap x X) ≡ₚ (., x) <$> elements X.
proof: Proof. induction X as [| y X not_in IH] using set_ind_L. - rewrite gset_to_gmap_empty, elements_empty, map_to_list_empty. done. - rewrite gset_to_gmap_union_singleton, elements_union_singleton by done. rewrite map_to_list_insert. 2:{ rewrite lookup_gset_to_gmap_None. done. } rewrite IH. done. Qed.
imports: stdpp(mapset pmap) stdpp(options)