renamed lemma l12 → coarser_partitions_covers, documented, cleaned up
factored insert_into_member_partition1 out of lemma l12