1\THEOREM DELETE_INSERT pred_sets
2|- !x y s.
3    (x INSERT s) DELETE y =
4    ((x = y) => s DELETE y | x INSERT (s DELETE y))
5\ENDTHEOREM
6