proved lemma coarser_partitions_with_list_distinct