Moves a paired universal quantification outwards through a disjunction.
DESCRIPTION
When applied to a term of the form (!p. t) \/ (!p. u), where no variables
from p are free in either t nor u, OR_PFORALL_CONV returns the theorem:
|- (!p. t) \/ (!p. u) = (!p. t \/ u)
FAILURE
OR_PFORALL_CONV fails if it is applied to a term not of the form
(!p. t) \/ (!p. u), or if it is applied to a term (!p. t) \/ (!p. u)
in which the variables from p are free in either t or u.