Package axiom-extensionality: Axiom of Extensionality
Information
| name | axiom-extensionality |
| version | 1.8 |
| description | Axiom of Extensionality |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2011-07-19 |
| requires | bool-def |
| show | Data.Bool |
Files
- Package tarball axiom-extensionality-1.8.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
- ∀
- ⊤
- Bool
Assumptions
⊦ ⊤ ⇔ (λp. p) = λp. p
⊦ (∀) = λp. p = λx. ⊤
⊦ let a d ← (λe. d e) = d in a = λb. (λc. c) = λc. c