lemma all_coarser_partitions_with_list_alt
lemma all_coarser_partitions_with_list_alt: removed one unneeded assumption