1\THEOREM SET_CASES pred_sets 2|- !s. (s = {{}}) \/ (?x t. (s = x INSERT t) /\ ~x IN t) 3\ENDTHEOREM 4