MK_EXISTS

Drule.MK_EXISTS : (thm -> thm)

Existentially quantifies both sides of a universally quantified equational theorem.

When applied to a theorem A |- !x. t1 = t2, the inference rule MK_EXISTS returns the theorem A |- (?x. t1) = (?x. t2).

       A |- !x. t1 = t2
   --------------------------  MK_EXISTS
    A |- (?x. t1) = (?x. t2)

Failure

Fails unless the theorem is a singly universally quantified equation.

See also

Thm.AP_TERM, Drule.EXISTS_EQ, Thm.GEN, Drule.LIST_MK_EXISTS, Drule.MK_ABS