When applied to a theorem A' |- ?p. t and a goal, CHOOSE_TAC adds
t[p'/p] to the assumptions of the goal, where p' is a variant of
the pair p which has no components free in the assumption list;
normally p' is just p.
A ?- u
==================== CHOOSE_TAC (A' |- ?q. t)
A u {t[p'/p]} ?- u