CONJ_FORALL_CONV : conv
STRUCTURE
unwindLib
SYNOPSIS
Moves universal quantifiers up through a tree of conjunctions.
LIBRARY
unwind
DESCRIPTION
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
FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_RIGHT_RULE
HOL  Trindemossen-1