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