SKOLEM_CONV : conv
# SKOLEM_THM;; val it : thm = |- !P. (!x. ?y. P x y) <=> (?y. !x. P x (y x))
# SKOLEM_CONV `(!x. ?y. P x y) \/ (?u. !v. ?z. P (f u v) z)`;; Warning: inventing type variables val it : thm = |- (!x. ?y. P x y) \/ (?u. !v. ?z. P (f u v) z) <=> (?y u z. (!x. P x (y x)) \/ (!v. P (f u v) (z v)))
# SKOLEM_CONV `(!x. ?y. P x y) ==> (?u. !v. ?z. P (f u v) z)`;; Warning: inventing type variables val it : thm = |- (!x. ?y. P x y) ==> (?u. !v. ?z. P (f u v) z) <=> (?y. !x. P x (y x)) ==> (?u z. !v. P (f u v) (z v))