OR_EXISTS_CONV : conv
STRUCTURE
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
HOL  Kananaskis-13