Function vstd::set::axiom_set_intersect
source · pub broadcast proof fn axiom_set_intersect<A>(s1: Set<A>, s2: Set<A>, a: A)Expand description
ensures
#[trigger] s1.intersect(s2).contains(a) == (s1.contains(a) && s2.contains(a)),The intersection of sets s1 and s2 contains element a if and only if
both s1 and s2 contain a.