for s being SynTypes_Calculus
for x being type of s holds
( <*> the carrier of s ==>. x /" x & <*> the carrier of s ==>. x \ x )