modified coarser_partitions_with_list to represent “all partitions” as 'a set list list (easier to handle)
lemma distinct_map