for X being StackAlgebra
for s1, s2, s3 being stack of X st s1 == s2 & s2 == s3 holds
s1 == s3 ;