X_CHOOSE_TAC : term -> thm_tactic
A ?- t =================== X_CHOOSE_TAC `y` (A1 |- ?x. w) A u {w[y/x]} ?- t (`y` not free anywhere)
# g `(?y. x = y + 2) ==> x < x * x`;;
# e(DISCH_THEN(X_CHOOSE_TAC `d:num`));; val it : goalstack = 1 subgoal (1 total) 0 [`x = d + 2`] `x < x * x`
# e(ASM_REWRITE_TAC[] THEN ARITH_TAC);; val it : goalstack = No subgoals