----------------------------------------------------------------------
CONJ_FORALL_CONV                                           (unwindLib)
----------------------------------------------------------------------
CONJ_FORALL_CONV : conv

SYNOPSIS
Moves universal quantifiers up through a tree of conjunctions.

LIBRARY
unwind

DESCRIBE
{CONJ_FORALL_CONV "(!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)"} returns the
following theorem:

   |- (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn) =
      !x1 ... xm. t1 /\ ... /\ 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

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

#CONJ_FORALL_CONV "T";;
|- T = T

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


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

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