CONJ_FORALL_RIGHT_RULE : (thm -> thm)
STRUCTURE
unwindLib
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
FORALL_CONJ_RIGHT_RULE, CONJ_FORALL_CONV, FORALL_CONJ_CONV, CONJ_FORALL_ONCE_CONV, FORALL_CONJ_ONCE_CONV
HOL  Trindemossen-1