prove map_size_delete, map_size_insert_Some, map_to_list_delete
All threads resolved!
All threads resolved!
Compare changes
map_size_insert_Some exists in Perennial as map_size_insert_overwrite, but with a very different proof.