SIGNATURE PairCompare[data1,data2]

-- comparing pairs

-- Parameter
SORT data1 data2

IMPORT Pair[data1,data2] ONLY pair
       RelCmp ONLY rel < = > <? =? >?

FUN cmp  : (data1 ** data1 -> bool) ** (data2 ** data2 -> bool)
                                -> pair ** pair -> rel
           -- cmp (<_1,<_2)(p1, p2)
           -- lexicographical lifting of <_n to pairs
           -- given a total, irreflexive order, produces
           -- such an order. 

FUN eq?  : (data1 ** data1 -> bool) ** (data2 ** data2 -> bool)
                                -> pair ** pair -> bool
           -- equality
           -- (should be used with an equivalence relation)