Package bool-ext: Extensional boolean theorems

Information

namebool-ext
version1.10
descriptionExtensional boolean theorems
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-11-12
requiresaxiom-extensionality
bool-def
bool-int
showData.Bool

Files

Theorems

f g. (x. f x = g x) f = g

f g. (x. f x = g x) f = g

Input Type Operators

Input Constants

Assumptions

t. t t

t. (λx. t x) = t

() = λp. p = λx.

() = λp q. p q p

() = λp q. (λf. f p q) = λf. f