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