MK_EXISTS : term -> thm -> thm
A |- p <=> q ---------------------------- MK_EXISTS `v` [where v not free in A] A |- (?v. p) <=> (?v. q)
# let th = ARITH_RULE `f(x:A) >= 1 <=> ~(f(x) = 0)`;; val th : thm = |- f x >= 1 <=> ~(f x = 0) # MK_EXISTS `x:A` th;; val it : thm = |- (?x. f x >= 1) <=> (?x. ~(f x = 0))