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