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