Function vstd::multiset::lemma_right_pseudo_idempotence

source ·

pub proof fn lemma_right_pseudo_idempotence<V>(a: Multiset<V>, b: Multiset<V>)

Expand description

ensures

a.intersection_with(a.intersection_with(b)) =~= a.intersection_with(b),

Taking the intersection of multiset a with the result of taking the intersection of a and b is the same as just taking the intersection of a and b once.