CHOOSE : term * thm -> thm -> thm
STRUCTURE
SYNOPSIS
Eliminates existential quantification using deduction from a particular witness.
DESCRIPTION
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
HOL  Kananaskis-13