Package axiom-extensionality: Axiom of Extensionality
Information
| name | axiom-extensionality |
| version | 1.9 |
| description | Axiom of Extensionality |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-10-30 |
| checksum | 6e9a7c8e10c21e54d5f3285cb11e65de99c9542d |
| requires | bool-def |
| show | Data.Bool |
Files
- Package tarball axiom-extensionality-1.9.tgz
- Theory source file axiom-extensionality.thy (included in the package tarball)
Theorem
⊦ ∀t. (λx. t x) = t
External Type Operators
- →
- bool
External Constants
- =
- Data
- Bool
- ∀
- ⊤
- Bool
Assumptions
⊦ AXIOM OF EXTENSIONALITY
⊦ ⊤ ⇔ (λp. p) = λp. p
⊦ (∀) = λp. p = λx. ⊤