EXISTS_EQUATION : term -> thm -> thm
# let th = (UNDISCH o EQT_ELIM o SIMP_CONV[ARITH]) `x = 3 ==> ODD(x) /\ x > 2`;; val th : thm = x = 3 |- ODD x /\ x > 2 # EXISTS_EQUATION `x = 3` th;; val it : thm = |- ?x. ODD x /\ x > 2
# EXISTS_EQUATION `x = 1` (REFL `x:num`);; val it : thm = |- ?x. x = x