FORALL_CONJ_RIGHT_RULE : (thm -> thm)
STRUCTURE
unwindLib
SYNOPSIS
Moves universal quantifiers down through a tree of conjunctions.
LIBRARY
unwind
DESCRIPTION
      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ tn
   -------------------------------------------------------------------
    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
FAILURE
Fails if the argument theorem is not of the required form, though either or both of r and p may be zero.
SEEALSO
CONJ_FORALL_RIGHT_RULE, FORALL_CONJ_CONV, CONJ_FORALL_CONV, FORALL_CONJ_ONCE_CONV, CONJ_FORALL_ONCE_CONV
HOL  Kananaskis-13