Function vstd::map::axiom_map_insert_same

source · 
pub broadcast proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)
Expand description
ensures
#[trigger] m.insert(key, value)[key] == value,

Inserting value at key in m results in a map that maps key to value