\DOC EXISTS_TAC

\TYPE {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.
\ENDDOC