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