Package axiom-extensionality: Axiom of Extensionality
Information
| name | axiom-extensionality |
| version | 1.4 |
| description | Axiom of Extensionality |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2011-07-19 |
| show | Data.Bool |
Files
- Package tarball axiom-extensionality-1.4.tgz
- Theory file axiom-extensionality.thy (included in the package tarball)
Theorem
⊦ ∀t. (λx. t x) = t
Input Type Operators
- →
- bool
Input Constants
- =
- Data
- Bool
- ∀
- T
- Bool
Assumptions
⊦ T ⇔ (λp. p) = λp. p
⊦ (∀) = λp. p = λx. T
⊦ let a d ← (λe. d e) = d in a = λb. (λc. c) = λc. c