Function is_partition 

pub open spec fn is_partition<A>(s: Set<A>, parts: Set<Set<A>>) -> bool

{
    (forall |part: Set<A>| {
        #[trigger] parts.contains(part) ==> !part.is_empty() && part <= s
    }) && pairwise_disjoint(parts) && s == parts.flatten()
}