----------------------------------------------------------------------
DEPTH_FORALL_CONV                                          (unwindLib)
----------------------------------------------------------------------
DEPTH_FORALL_CONV : (conv -> conv)

SYNOPSIS
Applies a conversion to the body of nested universal quantifications.

LIBRARY
unwind

DESCRIBE
{DEPTH_FORALL_CONV conv "!x1 ... xn. body"} applies {conv} to {"body"} and
returns a theorem of the form:

   |- (!x1 ... xn. body) = (!x1 ... xn. body')


FAILURE
Fails if the application of {conv} fails.

EXAMPLE

#DEPTH_FORALL_CONV BETA_CONV "!x y z. (\w. x /\ y /\ z /\ w) T";;
|- (!x y z. (\w. x /\ y /\ z /\ w)T) = (!x y z. x /\ y /\ z /\ T)


SEEALSO
unwindLib.DEPTH_EXISTS_CONV.

----------------------------------------------------------------------