1\DOC PEXT
2
3\TYPE {PEXT : (thm -> thm)}
4
5\KEYWORDS
6rule, extensionality.
7
8\LIBRARY
9pair
10
11\SYNOPSIS
12Derives equality of functions from extensional equivalence.
13
14\DESCRIBE
15When applied to a theorem {A |- !p. t1 p = t2 p},
16the inference rule {PEXT} returns the theorem {A |- t1 = t2}.
17{
18    A |- !p. t1 p = t2 p
19   ----------------------  PEXT          [where p is not free in t1 or t2]
20        A |- t1 = t2
21}
22
23
24\FAILURE
25Fails if the theorem does not have the form indicated above, or
26if any of the component variables in the paired variable structure {p}
27is free either of the functions {t1} or {t2}.
28
29\EXAMPLE
30{
31- PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`));
32> val it =  [.] |- f = g : thm
33}
34
35
36\SEEALSO
37Drule.EXT, Thm.AP_THM, PairRules.PETA_CONV, Conv.FUN_EQ_CONV, PairRules.P_FUN_EQ_CONV.
38\ENDDOC
39