Function vstd::multiset::axiom_multiset_empty

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

The empty multiset maps every element to multiplicity 0