λδ digital library (LDDL)
Constant
Informal description: ""
{λ[x:
nat
]
.
λ[a:Π[y:
nat
]
.
nat
]
.
λ[b:Π[y:
nat
]
.
nat
]
.
λ[pa:{(a)
.
(x)}
.
prop2
]
.
λ[pb:{(b)
.
(x)}
.
prop2
]
.
λ[y:
nat
]
.
λ[p:{(y)
.
(pb)
.
(pa)
.
(b)
.
(a)
.
(x)}
.
prop3
]}
.
<{((y)
.
suc
)
.
(pb)
.
(pa)
.
(b)
.
(a)
.
(x)}
.
prop3
>
.
{({({(p)
.
(y)
.
(pb)
.
(pa)
.
(b)
.
(a)
.
(x)}
.
t8
)
.
(((y)
.
b)
.
suc
)
.
(((y)
.
suc
)
.
b)
.
(
nat
)}
.
symis
)
.
({(p)
.
(y)
.
(pb)
.
(pa)
.
(b)
.
(a)
.
(x)}
.
t4
)
.
({(p)
.
(y)
.
(pb)
.
(pa)
.
(b)
.
(a)
.
(x)}
.
t7
)
.
(((y)
.
suc
)
.
b)
.
(((y)
.
b)
.
suc
)
.
(((y)
.
a)
.
suc
)
.
(((y)
.
suc
)
.
a)
.
(
nat
)}
.
tr3is
Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sun, 04 Jan 2015 22:01:49 +0100