1\THEOREM INSERT_COMM pred_sets 2|- !x y s. x INSERT (y INSERT s) = y INSERT (x INSERT s) 3\ENDTHEOREM 4