EXT : thm -> thm

- STRUCTURE
- 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

HOL Kananaskis-14