----------------------------------------------------------------------
FORALL_CONJ_CONV                                           (unwindLib)
----------------------------------------------------------------------
FORALL_CONJ_CONV : conv

SYNOPSIS
Moves universal quantifiers down through a tree of conjunctions.

LIBRARY
unwind

DESCRIBE
{FORALL_CONJ_CONV "!x1 ... xm. t1 /\ ... /\ tn"} returns the theorem:

   |- !x1 ... xm. t1 /\ ... /\ tn =
      (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)

where the original term can be an arbitrary tree of conjunctions. The
structure of the tree is retained in both sides of the equation.

FAILURE
Never fails.

EXAMPLE

#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). (a /\ b) /\ c";;
|- (!x y z. (a /\ b) /\ c) = ((!x y z. a) /\ (!x y z. b)) /\ (!x y z. c)

#FORALL_CONJ_CONV "T";;
|- T = T

#FORALL_CONJ_CONV "!(x:*) (y:*) (z:*). T";;
|- (!x y z. T) = (!x y z. T)


SEEALSO
unwindLib.CONJ_FORALL_CONV, unwindLib.FORALL_CONJ_ONCE_CONV,
unwindLib.CONJ_FORALL_ONCE_CONV, unwindLib.FORALL_CONJ_RIGHT_RULE,
unwindLib.CONJ_FORALL_RIGHT_RULE.

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