Function vstd::map::axiom_map_remove_domain
source · pub broadcast proof fn axiom_map_remove_domain<K, V>(m: Map<K, V>, key: K)Expand description
ensures
#[trigger] m.remove(key).dom() == m.dom().remove(key),The domain of a map after removing a key-value pair is equivalent to removing the key from the original map’s domain set.