Package bool-ext: Boolean extensionality theorems

Information

namebool-ext
version1.1
descriptionBoolean extensionality theorems
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-07-18
showData.Bool

Files

Theorems

f g. f = g x. f x = g x

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

Input Type Operators

Input Constants

Assumptions

T

t. (λx. t x) = t

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

() = λp q. p q p

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

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)