----------------------------------------------------------------------
EXT                                                            (Drule)
----------------------------------------------------------------------
EXT : thm -> thm

SYNOPSIS
Derives equality of functions from extensional equivalence.

KEYWORDS
rule, extensionality.

DESCRIBE
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
Thm.AP_THM, Drule.ETA_CONV, Conv.FUN_EQ_CONV.

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