Thinking that this kind of abstraction is better is rather silly,
since the two ways of defining stack are isomorphic and one can define
the "concrete" representation in terms of the "abstract" one.
You need an additional requirement--e.g., it's not true if you perform
all the pops first. Perhaps this illustrates the difficulty of using
algebraic specification.