new "'a set list list"↔"'a set set set" equivalence proofs for some definitions:
* insert_into_member_list_alt
* coarser_partitions_with_list_alt (also used this to simplify coarser_partitions_covers_list)