EXT : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Derives equality of functions from extensional equivalence.
DESCRIPTION
When applied to a theorem A |- !x. t1 x = t2 x, the inference rule EXT returns the theorem A |- t1 = t2. 
    A |- !x. t1 x = t2 x
   ----------------------  EXT          [where x is not free in t1 or t2]
        A |- t1 = t2

FAILURE
Fails if the theorem does not have the form indicated above, or if the variable x is free in either of the functions t1 or t2.
COMMENTS
This rule is expressed as an equivalence in the theorem boolTheory.FUN_EQ_THM.
SEEALSO
AP_THM, ETA_CONV, FUN_EQ_CONV
HOL  Trindemossen-1