pub broadcast proof fn lemma_iset_intersect_again2<A>(a: ISet<A>, b: ISet<A>)Expand description
ensures
(a.intersect(b)).intersect(a) =~= a.intersect(b),Taking the intersection of sets a and b and then taking the intersection of the result with a
is the same as taking the intersection of a and b once.