X_CHOOSE_THEN : term -> thm_tactical
A ?- t ========= ttac ({w[y/x]} |- w[y/x]) A ?- t1
A ?- t ========= X_CHOOSE_THEN `y` ttac (A1 |- ?x. w) A ?- t1 (`y` not free anywhere)
# g `!m n. m < n ==> m EXP 2 + 2 * m <= n EXP 2`;;
# e(REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS]);; val it : goalstack = 1 subgoal (1 total) `(?d. n = m + SUC d) ==> m EXP 2 + 2 * m <= n EXP 2`
# e(DISCH_THEN(X_CHOOSE_THEN `e:num` SUBST1_TAC));; val it : goalstack = 1 subgoal (1 total) `m EXP 2 + 2 * m <= (m + SUC e) EXP 2`