type s, t
op __ + __ : s * s -> s
op x1,x2:s
op y:s = (op x2:s) + (op x2:s)