a few more proves_IMP cases

ABS, BETA, ASSUME, EQ_MP