----------------------------------------------------------------------
EXISTS_TAC                                                    (Tactic)
----------------------------------------------------------------------
EXISTS_TAC : (term -> tactic)

SYNOPSIS
Reduces existentially quantified goal to one involving a specific witness.

KEYWORDS
tactic, quantifier, existential, choose, witness.

DESCRIBE
When applied to a term {u} and a goal {?x. t}, the tactic
{EXISTS_TAC} reduces the goal to {t[u/x]} (substituting {u}
for all free instances of {x} in {t}, with variable renaming if
necessary to avoid free variable capture).

    A ?- ?x. t
   =============  EXISTS_TAC "u"
    A ?- t[u/x]




FAILURE
Fails unless the goal’s conclusion is existentially quantified and the
term supplied has the same type as the quantified variable in the goal.

EXAMPLE
The goal:

   ?- ?x. x=T

can be solved by:

   EXISTS_TAC ``T`` THEN REFL_TAC


SEEALSO
Thm.EXISTS.

----------------------------------------------------------------------