When applied to a term already in negation normal form (see NNF_CONV, for
example), the conversion PRENEX_CONV proves it equal to an equivalent in
prenex form, with all quantifiers at the top level and a propositional body.
FAILURE CONDITIONS
Never fails; even on non-Boolean terms it will just produce a reflexive
theorem.
EXAMPLE
# PRENEX_CONV `(!x. ?y. P x y) \/ (?u. !v. ?w. Q u v w)`;;
Warning: inventing type variables
val it : thm =
|- (!x. ?y. P x y) \/ (?u. !v. ?w. Q u v w) <=>
(!x. ?y u. !v. ?w. P x y \/ Q u v w)