Function vstd::multiset::lemma_left_pseudo_idempotence
source · pub proof fn lemma_left_pseudo_idempotence<V>(a: Multiset<V>, b: Multiset<V>)Expand description
ensures
a.intersection_with(b).intersection_with(b) =~= a.intersection_with(b),Taking the intersection of multisets a and b and then taking the resulting multiset’s intersection
with b again is the same as just taking the intersection of a and b once.