OR_EXISTS_CONV : conv
STRUCTURE
Conv
SYNOPSIS
Moves an existential quantification outwards through a disjunction.
DESCRIPTION
When applied to a term of the form (?x.P) \/ (?x.Q), the conversion OR_EXISTS_CONV returns the theorem: 
   |- (?x.P) \/ (?x.Q) = (?x. P \/ Q)

FAILURE
Fails if applied to a term not of the form (?x.P) \/ (?x.Q).
SEEALSO
EXISTS_OR_CONV, LEFT_OR_EXISTS_CONV, RIGHT_OR_EXISTS_CONV
HOL  Kananaskis-13