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
pub broadcast proof fn axiom_multiset_empty<V>(v: V)#[trigger] Multiset::empty().count(v) == 0,The empty multiset maps every element to multiplicity 0