CONJ_FORALL_RIGHT_RULE : (thm -> thm)
STRUCTURE
SYNOPSIS
Moves universal quantifiers up through a tree of conjunctions.
LIBRARY
unwind
DESCRIPTION
    A |- !z1 ... zr.
          t = ?y1 ... yp. (!x1 ... xm. t1) /\ ... /\ (!x1 ... xm. tn)
   -------------------------------------------------------------------
      A |- !z1 ... zr. t = ?y1 ... yp. !x1 ... xm. t1 /\ ... /\ 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
HOL  Trindemossen-1