λδ digital library (LDDL)
Constant
Informal description: ""
{λ[sigma:Set]
.
λ[r:∀[x:sigma]
.
∀[y:sigma]
.
Prop]
.
λ[refr1:∀[x:sigma]
.
(x)
.
(x)
.
r]
.
λ[symr1:∀[x:sigma]
.
∀[y:sigma]
.
∀[t:(y)
.
(x)
.
r]
.
(x)
.
(y)
.
r]
.
λ[trr1:∀[x:sigma]
.
∀[y:sigma]
.
∀[z:sigma]
.
∀[t:(y)
.
(x)
.
r]
.
∀[u:(z)
.
(y)
.
r]
.
(z)
.
(x)
.
r]
.
λ[alpha:Set]
.
λ[fu:Π[x:sigma]
.
alpha]
.
λ[ff:{(fu)
.
(alpha)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
fixfu
]
.
λ[e:{(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ect
]
.
λ[a1:alpha]
.
λ[s:sigma]}
.
<Prop>
.
{({(a1)
.
((s)
.
fu)
.
(alpha)}
.
is
)
.
({({(e)
.
(trr1)
.
(symr1)
.
(refr1)
.
(r)
.
(sigma)}
.
ecect
)
.
(s)
.
(sigma)}
.
esti
)}
.
and
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 21:59:28 +0100