MK_FORALL : term -> thm -> thm
A |- p <=> q ---------------------------- MK_FORALL `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_FORALL `x:A` th;; val it : thm = |- (!x. f x >= 1) <=> (!x. ~(f x = 0))