LEFT_IMP_PEXISTS_CONV : conv

- STRUCTURE
- SYNOPSIS
- Moves a paired existential quantification of the antecedent outwards through an implication.
- DESCRIPTION
- When applied to a term of the form (?p. t) ==> u, the conversion LEFT_IMP_PEXISTS_CONV returns the theorem:where p' is a primed variant of the pair p that does not contain any variables that appear free in the input term.
|- (?p. t) ==> u = (!p'. t[p'/p] ==> u)

- FAILURE
- Fails if applied to a term not of the form (?p. t) ==> u.
- SEEALSO

HOL Kananaskis-14