{
[eq,x,v,y:Top].
(x
:
v(y)
~
v)
}
{
Proof
}
Definitions occuring in Statement
:
fpf-single:
x
:
v
,
fpf-ap:
f(x)
,
uall:
[x:A].
B[x]
,
top:
Top
,
sqequal:
s
~
t
Definitions
:
member:
t
T
,
fpf-ap:
f(x)
,
fpf-single:
x
:
v
,
pi2:
snd(t)
Lemmas
:
top_wf
\mforall{}[eq,x,v,y:Top]. (x : v(y) \msim{} v)
Date html generated: 2011_08_10-AM-08_03_04
Last ObjectModification: 2011_06_18-AM-08_20_51
Home
Index
[x:A]. B[x], [eq,x,v,y:Top]. (x : v(y) ~ v) }[x:A]. B[x], 
T,