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