OR_PFORALL_CONV : conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
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.
SEEALSO
HOL  Trindemossen-1