Function vstd::set_lib::lemma_set_union_again2

pub proof fn lemma_set_union_again2<A>(a: Set<A>, b: Set<A>)

Expand description

ensures

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.

Function vstd::set_lib::lemma_set_union_again2Copy item path