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