PEXT
PairRules.PEXT : (thm -> thm)
Derives equality of functions from extensional equivalence.
When applied to a theorem A |- !p. t1 p = t2 p, the inference rule
PEXT returns the theorem A |- t1 = t2.
A |- !p. t1 p = t2 p
---------------------- PEXT [where p is not free in t1 or t2]
A |- t1 = t2
Failure
Fails if the theorem does not have the form indicated above, or if any
of the component variables in the paired variable structure p is free
either of the functions t1 or t2.
Example
> PairRules.PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`));
val it = [.] ⊢ f = g: thm
See also
Drule.EXT, Thm.AP_THM,
PairRules.PETA_CONV,
Conv.FUN_EQ_CONV,
PairRules.P_FUN_EQ_CONV