STRUCT_CASES_THEN : thm_tactic -> thm_tactic
th = A' |- ?y11...y1m. x = t1 /\ (B11 /\ ... /\ B1k) \/ ... \/ ?yn1...ynp. x = tn /\ (Bn1 /\ ... /\ Bnp)
# g `n > 0 ==> PRE(n) + 1 = n`;;
# e(STRUCT_CASES_THEN ASSUME_TAC (SPEC `n:num` num_CASES));; val it : goalstack = 2 subgoals (2 total) 0 [`n = SUC n'`] `n > 0 ==> PRE n + 1 = n` 0 [`n = 0`] `n > 0 ==> PRE n + 1 = n`