Add lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_{l,r}