delete some commented out stuff, fix proof by reordering defs
prove ABS_correct