Function vstd::set_lib::lemma_set_intersect_again2

source ·

pub proof fn lemma_set_intersect_again2<A>(a: Set<A>, b: Set<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.