Function lemma_hashmap_deepview_domCopy item path

pub broadcast proof fn lemma_hashmap_deepview_dom<K: DeepView, V: DeepView>(m: HashMap<K, V>)

#[trigger] m.deep_view().dom() == m@.dom().map(|k: K| k.deep_view()),