Function lemma_btree_map_deepview_dom Copy item path

pub broadcast proof fn lemma_btree_map_deepview_dom<K: DeepView, V: DeepView>(m: BTreeMap<K, V>)

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