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