CHOOSE_THEN : thm_tactical
A ?- s1 ========= ttac (t[x'/x] |- t[x'/x]) B ?- s2
A ?- s1 ========== CHOOSE_THEN ttac (A' |- ?x. t) B ?- s2
LT_EXISTS = |- !m n. m < n <=> (?d. n = m + SUC d)
# g `x < y ==> 0 < y * y`;;
# e(DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LT_EXISTS]));;
val it : goalstack = 1 subgoal (1 total) `0 < (x + SUC d) * (x + SUC d)`
# e(REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LT_0]);;