pub broadcast proof fn axiom_spec_btree_keys_iter<'a, Key, A: Allocator + Clone>(
m: &'a BTreeSet<Key, A>,
)Expand description
ensures
(#[trigger] spec_btree_keys_iter(m).remaining()).unref().to_set() == m@,spec_btree_keys_iter(m).remaining().no_duplicates(),spec_btree_keys_iter(m).remaining().len() == m@.len(),increasing_seq(spec_btree_keys_iter(m).remaining()),