SUBGOAL_TAC : string -> term -> tactic list -> tactic
# g `(n MOD 2) IN {0,1}`;;
# e(SUBGOAL_TAC "ml2" `n MOD 2 < 2` [SIMP_TAC[DIVISION; ARITH]]);; val it : goalstack = 1 subgoal (1 total) 0 [`n MOD 2 < 2`] (ml2) `n MOD 2 IN {0, 1}`
# e(REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN POP_ASSUM MP_TAC THEN ARITH_TAC);; val it : goalstack = No subgoals