lemma_btree_map_deepview_values

vstd::std_specs::btree

Function lemma_btree_map_deepview_values 

Source 
pub broadcast proof fn lemma_btree_map_deepview_values<K: DeepView, V: DeepView>(
    m: BTreeMap<K, V>,
)
Expand description
requires
crate::relations::injective(|k: K| k.deep_view()),
ensures
#[trigger] m.deep_view().values() =~= m@.values().map(|v: V| v.deep_view()),