pub broadcast proof fn lemma_iset_union_again2<A>(a: ISet<A>, b: ISet<A>)Expand description
ensures
#[trigger] a.union(b).union(a) =~= a.union(b),Taking the union of sets a and b and then taking the union of the result with a
is the same as taking the union of a and b once.