pub broadcast proof fn axiom_spec_values_iter<'a, Key, Value, A: Allocator + Clone>(
m: &'a BTreeMap<Key, Value, A>,
)Expand description
ensures
(#[trigger] spec_values_iter(m).remaining()).unref().to_set() == m@.values(),spec_values_iter(m).remaining().len() == m@.dom().len(),