Package axiom-extensionality: axiom-extensionality
Information
name
axiom-extensionality
version
1.0
description
axiom-extensionality
author
Joe Hurd <joe@gilith.com>
license
HOLLight
provenance
HOL Light theory extracted on 2011-02-19
show
Data.Bool
Files
Package tarball
axiom-extensionality-1.0.tgz
Theory file
axiom-extensionality.thy
(included in the package tarball)
Theorem
⊦
∀
t
. (
λ
x
.
t
x
)
=
t
Input Type Operators
→
bool
Input Constants
=
Data
Bool
∀
Assumption
⊦
∀
t
. (
λ
x
.
t
x
)
=
t