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