Proof of mset_mem_mon_for_union