Function vstd::multiset::axiom_len_add
source · pub broadcast proof fn axiom_len_add<V>(m1: Multiset<V>, m2: Multiset<V>)Expand description
ensures
(#[trigger] m1.add(m2).len()) == m1.len() + m2.len(),The length of the addition of two multisets is equal to the sum of the lengths of each individual multiset.