CHOOSE_TAC : thm_tactic
A ?- u ==================== CHOOSE_TAC (A' |- ?x. t) A u {t[x'/x]} ?- u
?- ?t. output(t)
t1 = |- ?t. input(t) t2 = !t. input(t) ==> output(t+1)
CHOOSE_TAC t1 THEN EXISTS_TAC `t+1` THEN UNDISCH_TAC `input (t:num) :bool` THEN MATCH_ACCEPT_TAC t2