pub broadcast proof fn axiom_hashmap_decreases<Key, Value, S>(m: HashMap<Key, Value, S>)
#[trigger] (decreases_to!(m => m @)),