vstd::std_specs::hash

Function axiom_hashmap_view_finite_dom

Source 
pub broadcast proof fn axiom_hashmap_view_finite_dom<K, V>(m: HashMap<K, V>)
Expand description
ensures
#[trigger] m@.dom().finite(),

A Map constructed from a HashMap is always finite.