axiom_btree_map_view_finite_dom

vstd::std_specs::btree

Function axiom_btree_map_view_finite_dom 

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

A Map constructed from a BTreeMap is always finite.