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