PTS *:* (*,*,*);
let
    #include <EqType.pts>
    #include <pair.pts>

    t (a:*) (b:*) (c:*) (d:*) (eq: EqType (Pair a b) (Pair c d)) : EqType a c;

in  *