1\DOC EXT
2
3\TYPE {EXT : thm -> thm}
4
5\SYNOPSIS
6Derives equality of functions from extensional equivalence.
7
8\KEYWORDS
9rule, extensionality.
10
11\DESCRIBE
12When applied to a theorem {A |- !x. t1 x = t2 x}, the inference rule
13{EXT} returns the theorem {A |- t1 = t2}.
14{
15    A |- !x. t1 x = t2 x
16   ----------------------  EXT          [where x is not free in t1 or t2]
17        A |- t1 = t2
18}
19
20
21\FAILURE
22Fails if the theorem does not have the form indicated above, or
23if the variable {x} is free in either of the functions {t1} or {t2}.
24
25\COMMENTS
26This rule is expressed as an equivalence in the theorem
27{boolTheory.FUN_EQ_THM}.
28
29\SEEALSO
30Thm.AP_THM, Drule.ETA_CONV, Conv.FUN_EQ_CONV.
31
32\ENDDOC
33