Function lemma_set_prop_mutual_exclusion Copy item path

pub proof fn lemma_set_prop_mutual_exclusion<A>(s: Set<A>, f: FnSpec<(A,), bool>)

s.finite(),

set_prop_mutual_exclusion(s, f) <==> s.filter(f).len() <= 1,