Package unit-thm: unit-thm

Information

nameunit-thm
version1.0
descriptionunit-thm
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-02-19
showData.Bool

Files

Theorems

f g. f = g

e. fn. fn Data.Unit.() = e

e. ∃!fn. fn Data.Unit.() = e

P. P Data.Unit.() x. P x

Input Type Operators

Input Constants

Assumptions

T

v. v = Data.Unit.()

t. (x. t) t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

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

() = λP. q. (x. P x q) q

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

P. (∃!x. P x) (x. P x) x x'. P x P x' x = x'

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

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