pub broadcast proof fn axiom_spec_keys_iter<'a, Key, Value, S, A: Allocator>(
m: &'a HashMap<Key, Value, S, A>,
)Expand description
ensures
(#[trigger] spec_keys_iter(m).remaining()).unref().to_set() == m@.dom(),spec_keys_iter(m).remaining().no_duplicates(),spec_keys_iter(m).remaining().len() == m@.dom().len(),