Function vstd::set::axiom_set_union

pub broadcast proof fn axiom_set_union<A>(s1: Set<A>, s2: Set<A>, a: A)

Expand description

ensures

#[trigger] s1.union(s2).contains(a) == (s1.contains(a) || s2.contains(a)),

The union of sets s1 and s2 contains element a if and only if s1 contains a and/or s2 contains a.

Function vstd::set::axiom_set_unionCopy item path