EXISTS_EQ

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

Existentially quantifies both sides of an equational theorem.

When applied to a variable x and a theorem whose conclusion is equational, A |- t1 = t2, the inference rule EXISTS_EQ returns the theorem A |- (?x. t1) = (?x. t2), provided the variable x is not free in any of the assumptions.

         A |- t1 = t2
   ------------------------  EXISTS_EQ "x"      [where x is not free in A]
    A |- (?x.t1) = (?x.t2)

Failure

Fails unless the theorem is equational with both sides having type bool, or if the term is not a variable, or if the variable to be quantified over is free in any of the assumptions.

See also

Thm.AP_TERM, Drule.EXISTS_IMP, Drule.FORALL_EQ, Drule.MK_EXISTS, Drule.SELECT_EQ