Package unit-thm: Properties of the unit type

Information

nameunit-thm
version1.11
descriptionProperties of the unit type
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-02-03
requiresbool
unit-def
showData.Bool
Data.Unit

Files

Theorems

f g. f = g

e. fn. fn () = e

e. ∃!fn. fn () = e

p. p () x. p x

Input Type Operators

Input Constants

Assumptions

t. t t

v. v = ()

t. (x. t) t

() = λp. p = λx.

t. t t

() = λp q. p q p

x y. x = y y = x

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

() = λp. q. (x. p x q) q

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

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