1\DOC CHOOSE 2 3\TYPE {CHOOSE : term * thm -> thm -> thm} 4 5\SYNOPSIS 6Eliminates existential quantification using deduction from a 7particular witness. 8 9\KEYWORDS 10rule, existential. 11 12\DESCRIBE 13When applied to a term-theorem pair {(v,A1 |- ?x. s)} and a second 14theorem of the form {A2 u {s[v/x]} |- t}, the inference rule {CHOOSE} 15produces the theorem {A1 u A2 |- t}. 16{ 17 A1 |- ?x. s A2 u {s[v/x]} |- t 18 --------------------------------------- CHOOSE (v,(A1 |- ?x. s)) 19 A1 u A2 |- t 20} 21Where {v} is not free in {A1}, {A2} or {t}. 22 23\FAILURE 24Fails unless the terms and theorems correspond as indicated above; in 25particular {v} must have the same type as the variable existentially 26quantified over, and must not be free in {A1}, {A2} or {t}. 27 28\SEEALSO 29Tactic.CHOOSE_TAC, Thm.EXISTS, Tactic.EXISTS_TAC, Drule.SELECT_ELIM. 30\ENDDOC 31