PEXISTS_EQ
PairRules.PEXISTS_EQ : (term -> thm -> thm)
Existentially quantifies both sides of an equational theorem.
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.
See also
Drule.EXISTS_EQ,
PairRules.PEXISTS_IMP,
PairRules.PFORALL_EQ,
PairRules.MK_PEXISTS,
PairRules.PSELECT_EQ