Prove theorem about delete of gset_to_gmap
Basically the opposite of gset_to_gmap_union_singleton.
I was going to call this gset_to_gmap_delete but I decided to follow the convention from the other lemma (which isn't called gset_to_gmap_insert).
