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