Package axiom-extensionality: axiom-extensionality

Information

nameaxiom-extensionality
version1.3
descriptionaxiom-extensionality
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-19
showData.Bool

Files

Theorem

t. (λx. t x) = t

Input Type Operators

Input Constants

Assumptions

T (λp. p) = λp. p

() = λp. p = λx. T

let a d ← (λe. d e) = da = λb. (λc. c) = λc. c