It would be nice if the stack refinement could be proven with logically atomic rules for the Treiber stack.
