Drule.SELECT

`SELECT_EQ`

Drule.SELECT_EQ : (term -> thm -> thm)

Applies epsilon abstraction to both terms of an equation.

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)

Fails if the conclusion of the theorem is not an equation, or if the variable x is free in A.

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