vstd::std_specs::hash

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 @)),