proposition: Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y : gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
proof: Proof. apply map_eq; intros j; apply option_eq; intros y. rewrite lookup_delete_Some, !lookup_gset_to_gmap_Some, elem_of_difference, elem_of_singleton; destruct (decide (i = j)); intuition. Qed.
imports: stdpp(mapset pmap) stdpp(options)