1deltype num 2delconst SUC 3delconst 0 4skipthm num_TY_DEF 5skipthm num_ISO_DEF 6skipthm SUC_DEF 7skipthm ZERO_DEF 8delproof NOT_SUC 9delproof INV_SUC 10delproof INDUCTION 11