pub proof fn lemma_set_separation<T>(s: Set<T>, f: FnSpec<(T,), bool>)Expand description
ensures
s.filter(f).disjoint(s.filter(|x| !f(x))),s == s.filter(f) + s.filter(|x| !f(x)),s.filter(f).len() + s.filter(|x| !f(x)).len() == s.len(),A finite set can be separated by a predicate into two disjoint sets.