pub broadcast proof fn axiom_hashmap_view_finite_dom<K, V>(m: HashMap<K, V>)
#[trigger] m@.dom().finite(),
A Map constructed from a HashMap is always finite.
Map
HashMap