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