Function lemma_is_partition_empty_parts 

pub proof fn lemma_is_partition_empty_parts<A>(s: Set<A>)

ensures

is_partition(s, Set::<Set<A>>::empty()) == s.is_empty(),

With no parts, s is a partition exactly when it is empty.