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