Can someone sanity check me on the code on pages 334-5? Does the method push really need !empty in its in contract? I might not be fully awake yet >< A...