1delconst NONE 2delconst SOME 3delconst IS_SOME 4delconst IS_NONE 5delconst OPTION_MAP 6deltype option 7skipthm option_TY_DEF 8skipthm datatype_option 9skipthm option_REP_ABS_DEF 10skipthm NONE_DEF 11skipthm SOME_DEF 12delproof option_Axiom 13delproof option_induction 14delproof option_nchotomy 15delproof SOME_11 16delproof NOT_NONE_SOME 17delproof NOT_SOME_NONE 18