1\THEOREM DIFF_INSERT pred_sets
2|- !s t x. s DIFF (x INSERT t) = (s DELETE x) DIFF t
3\ENDTHEOREM
4