Function axiom_map_decreases_to_entry 

pub broadcast proof fn axiom_map_decreases_to_entry<K, V>(m: Map<K, V>, key: K)

requires

m.dom().contains(key),

ensures

#[trigger] (decreases_to!(m => (key, m[key]))),