Function vstd::map::axiom_map_remove_different

source · 
pub broadcast proof fn axiom_map_remove_different<K, V>(m: Map<K, V>, key1: K, key2: K)
Expand description
requires
m.dom().contains(key1),
key1 != key2,
ensures
#[trigger] m.remove(key2)[key1] == m[key1],

Removing a key-value pair from a map does not change the value mapped to by any other keys in the map.