for s being SynTypes_Calculus
for x, y, z being type of s holds x /" (z * y) <==>. (x /" y) /" z