for X being StackAlgebra
for s1, s2 being stack of X st s1 == s2 & not emp s1 holds
top s1 = top s2