add gset_to_gmap_to_list

This came up while trying to convert an own of a map into a big_sepL of its elements.

stdpp/gmap.v

@@ -354,6 +354,17 @@ Section gset.
     apply map_eq; intros k. apply option_eq; intros y.
     rewrite lookup_gset_to_gmap_Some, lookup_set_to_map; naive_solver.
   Qed.
+
+  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.
+    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.
 End gset.
 
 Typeclasses Opaque gset.