Function vstd::map::axiom_map_insert_different

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

Inserting value at key2 does not change the value mapped to by any other keys in m