OR_PFORALL_CONV
PairRules.OR_PFORALL_CONV : conv
Moves a paired universal quantification outwards through a disjunction.
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.
See also
Conv.OR_FORALL_CONV,
PairRules.PFORALL_OR_CONV,
PairRules.LEFT_OR_PFORALL_CONV,
PairRules.RIGHT_OR_PFORALL_CONV