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

FAILURE
Fails if the theorem does not have the form indicated above, or if any of the component variables in the paired variable structure p is free either of the functions t1 or t2.
EXAMPLE
- PEXT (ASSUME (Term `!(x,y). ((f:('a#'a)->'a) (x,y)) = (g (x,y))`));
> val it =  [.] |- f = g : thm

SEEALSO
HOL  Trindemossen-1