pub proof fn lemma_set_separation<T>(s: Set<T>, f: FnSpec<(T,), bool>)Expand description
requires
s.finite(),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 disjoiint sets.