axiom_btree_set_decreases

vstd::std_specs::btree

Function axiom_btree_set_decreases 

Source 
pub broadcast proof fn axiom_btree_set_decreases<Key, A: Allocator + Clone>(m: BTreeSet<Key, A>)
Expand description
ensures
#[trigger] (decreases_to!(m => m @)),