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.