Function vstd::multiset::axiom_multiset_contained
source · pub broadcast proof fn axiom_multiset_contained<V>(m: Map<V, nat>, v: V)Expand description
requires
m.dom().finite(),m.dom().contains(v),#[trigger] Multiset::from_map(m).count(v) == m[v],A call to Multiset::new with input map m will return a multiset that maps
value v to multiplicity m[v] if v is in the domain of m.