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.