FORALL_CONJ_CONV : conv
STRUCTURE
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
HOL  Kananaskis-13