\DOC CHOOSE

\TYPE {CHOOSE : term * thm -> thm -> thm}

\SYNOPSIS
Eliminates existential quantification using deduction from a
particular witness.

\KEYWORDS
rule, existential.

\DESCRIBE
When applied to a term-theorem pair {(v,A1 |- ?x. s)} and a second
theorem of the form {A2 u {s[v/x]} |- t}, the inference rule {CHOOSE}
produces the theorem {A1 u A2 |- t}.
{
    A1 |- ?x. s        A2 u {s[v/x]} |- t
   ---------------------------------------  CHOOSE (v,(A1 |- ?x. s))
                A1 u A2 |- t
}
Where {v} is not free in {A1}, {A2} or {t}.

\FAILURE
Fails unless the terms and theorems correspond as indicated above; in
particular {v} must have the same type as the variable existentially
quantified over, and must not be free in {A1}, {A2} or {t}.

\SEEALSO
Tactic.CHOOSE_TAC, Thm.EXISTS, Tactic.EXISTS_TAC, Drule.SELECT_ELIM.
\ENDDOC