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