set_prop_mutual_exclusion

vstd_extra::set_extra

Function set_prop_mutual_exclusion 

Source 
pub open spec fn set_prop_mutual_exclusion<A>(s: Set<A>, f: FnSpec<(A,), bool>) -> bool
Expand description
{
    forall |x: A, y: A| {
        #[trigger] s.contains(x) && #[trigger] s.contains(y) && x != y
            ==> !(f(x) && f(y))
    }
}