pairwise_disjoint

vstd_extra::set_extra

Function pairwise_disjoint 

Source 
pub open spec fn pairwise_disjoint<A>(sets: Set<Set<A>>) -> bool
Expand description
{
    forall |s1: Set<A>, s2: Set<A>| {
        sets.contains(s1) && sets.contains(s2) && s1 != s2 ==> s1.disjoint(s2)
    }
}

A set of sets is pairwise disjoint if all distinct sets are disjoint.