proved all_partitions_of_list_list_distinct, leaving coarser_partitions_with_list_distinct as a new, simpler proof obligation