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