Function vstd::multiset::axiom_multiset_ext_equal

pub broadcast proof fn axiom_multiset_ext_equal<V>(m1: Multiset<V>, m2: Multiset<V>)

Expand description

ensures

#[trigger] (m1 =~= m2) <==> (forall |v: V| m1.count(v) == m2.count(v)),

Two multisets are equivalent if and only if they have the same count for every value.