Function lemma_from_map_dom

pub broadcast proof fn lemma_from_map_dom<V>(mymap: Map<V, nat>)

Expand description

requires

forall |k| #[trigger] mymap.contains_key(k) ==> mymap[k] > 0,

ensures

#[trigger] Multiset::from_map(mymap).dom() == mymap.dom(),

lemma_from_map_dom