Skip to content

Prove theorem about delete of gset_to_gmap

Tej Chajed requested to merge tchajed/stdpp:gset-gmap-delete into master

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

Merge request reports