pub broadcast proof fn axiom_spec_hash_map_len<Key, Value, S, A: Allocator>(
m: &HashMap<Key, Value, S, A>,
)Expand description
ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
==> #[trigger] spec_hash_map_len(m) == m@.len(),