{
[X,es:Top].
(X([])
~
[])
}
{
Proof
}
Definitions occuring in Statement
:
eclass-vals:
X(L)
,
uall:
[x:A].
B[x]
,
top:
Top
,
nil:
[]
,
sqequal:
s
~
t
Definitions
:
uall:
[x:A].
B[x]
,
eclass-vals:
X(L)
,
member:
t
T
,
map:
map(f;as)
,
ycomb:
Y
Lemmas
:
top_wf
\mforall{}[X,es:Top]. (X([]) \msim{} [])
Date html generated: 2011_08_16-PM-04_08_43
Last ObjectModification: 2011_06_20-AM-00_42_08
Home
Index
[x:A]. B[x], [X,es:Top]. (X([]) ~ []) }[x:A]. B[x], [x:A]. B[x], 
T,