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