HOL-ex.List_to_Set_Comprehension_Examples