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).