pub broadcast proof fn lemma_right_pseudo_idempotence<V>(a: Multiset<V>, b: Multiset<V>)Expand description
ensures
#[trigger] 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.