Function vstd::multiset::axiom_multiset_singleton
source · pub broadcast proof fn axiom_multiset_singleton<V>(v: V)Expand description
ensures
(#[trigger] Multiset::singleton(v)).count(v) == 1,A call to Multiset::singleton with input value v will return a multiset that maps
value v to multiplicity 1.