SELECT_EQ : (term -> thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Applies epsilon abstraction to both terms of an equation.
DESCRIPTION
Effects the extensionality of the epsilon operator @. 
       A |- t1 = t2
   ------------------------  SELECT_EQ "x"      [where x is not free in A]
    A |- (@x.t1) = (@x.t2)

FAILURE
Fails if the conclusion of the theorem is not an equation, or if the variable x is free in A.
EXAMPLE
Given a theorem which shows the equivalence of two distinct forms of defining the property of being an even number: 
   th = |- (x MOD 2 = 0) = (?y. x = 2 * y)
A theorem giving the equivalence of the epsilon abstraction of each form is obtained: 
   - SELECT_EQ (Term `x:num`) th;
   > val it = |- (@x. x MOD 2 = 0) = (@x. ?y. x = 2 * y) : thm

SEEALSO
ABS, AP_TERM, EXISTS_EQ, FORALL_EQ, SELECT_CONV, SELECT_ELIM, SELECT_INTRO
HOL  Kananaskis-13