PEXISTS_EQ : (term -> thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Existentially quantifies both sides of an equational theorem.
- DESCRIPTION
- When applied to a paired structure of variables p and a theorem whose conclusion is equational:
A |- t1 = t2

the inference rule PEXISTS_EQ returns the theorem:

A |- (?p. t1) = (?p. t2)

provided the none of the variables in p is not free in any of the assumptions.

A |- t1 = t2 -------------------------- PEXISTS_EQ "p" [where p is not free in A] A |- (?p. t1) = (?p. t2)

- FAILURE
- Fails unless the theorem is equational with both sides having type bool, or if the term is not a paired structure of variables, or if any variable in the pair to be quantified over is free in any of the assumptions.
- SEEALSO

HOL Kananaskis-14