----------------------------------------------------------------------
PEXT                                                       (PairRules)
----------------------------------------------------------------------
PEXT : (thm -> thm)

KEYWORDS
rule, extensionality.

LIBRARY
pair

SYNOPSIS
Derives equality of functions from extensional equivalence.

DESCRIBE
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

- PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`));
> val it =  [.] |- f = g : thm




SEEALSO
Drule.EXT, Thm.AP_THM, PairRules.PETA_CONV, Conv.FUN_EQ_CONV,
PairRules.P_FUN_EQ_CONV.

----------------------------------------------------------------------