1\THEOREM INSERT_DIFF pred_sets 2|- !s t x. 3 (x INSERT s) DIFF t = (x IN t => s DIFF t | x INSERT (s DIFF t)) 4\ENDTHEOREM 5