Add lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_{l,r}

Thanks for the MR. I left a comment for one lemma. I think the other two lemmas are fine.

added 1 commit

• efe73fee - Add lemmas elem_of_list_to_set_disj and gmultiset_difference_disj_union_{l,r}

Compare with previous version

resolved all threads

resolved all threads

added 1 commit

• fa7c7f01 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

enabled an automatic merge when the pipeline for fa7c7f01 succeeds

Thanks. Going to merge.

merged

mentioned in commit 17d49675