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

in * -- \ (s:*) . \ (t:*) . \ u:* . \ st:EqType s t . \ tu:EqType t u . tu (\ x:* . EqType s x) st