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