Function axiom_hashset_decreases

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