set.mem_of_mem_of_subset source