HOL-ex.Set_Comprehension_Pointfree_Examples