λδ digital library (LDDL)
Constant
Informal description: ""
λ[x:
nat
]
.
<{(
1
)
.
(x)}
.
prop1
>
.
{(λ[z:{(
1
)
.
(x)}
.
nis
]
.
{(z)
.
(x)}
.
t16a
)
.
(λ[z:{(
1
)
.
(x)}
.
is
]
.
{(z)
.
(x)}
.
t12
)
.
({(
1
)
.
(x)}
.
prop1
)
.
({(
1
)
.
(x)}
.
is
)}
.
th1
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 22:03:18 +0100