SIGNATURE SetConstr[data1 , < :data1 ** data1 -> bool, data2, 

                           < :data2 ** data2 -> bool]
-- constructing sets from other sets

-- Parameter
SORT data1 data2
FUN < :data1 ** data1 -> bool
FUN < :data2 ** data2 -> bool

IMPORT Set[data1, <] ONLY set
       Set[data2, <] ONLY set
       Pair[data1, data2] ONLY pair
       Union2[data1, data2] ONLY union
       Set[pair[data1, data2], <] ONLY set
       Set[union[data1, data2], <] ONLY set
       
-- cartesian product
FUN x : set[data1, <] ** set[data2, <] -> set[pair, <]
-- x in A and y in B <=> x & y in A x B

FUN < : pair ** pair -> bool

-- disjoint union
FUN U : set[data1, <] ** set[data2, <] -> set[union, <]
-- x in A and y in B <=> data1(x) in A U B and data2(y) in A U B

FUN < : union ** union -> bool