Function vstd::multiset::axiom_multiset_singleton_different

source · 
pub broadcast proof fn axiom_multiset_singleton_different<V>(v: V, w: V)
Expand description
ensures
v != w ==> #[trigger] Multiset::singleton(v).count(w) == 0,

A call to Multiset::singleton with input value v will return a multiset that maps any value other than v to 0