Function vstd::multiset::axiom_multiset_add
source · pub broadcast proof fn axiom_multiset_add<V>(m1: Multiset<V>, m2: Multiset<V>, v: V)Expand description
ensures
#[trigger] m1.add(m2).count(v) == m1.count(v) + m2.count(v),The count of value v in the multiset m1.add(m2) is equal to the sum of the
counts of v in m1 and m2 individually.