{
[es,B,I:Top].
({e:E|
{I}
e}
~
E(I))
}
{
Proof
}
Definitions occuring in Statement
:
es-E-interface:
E(X)
,
es-interface-predicate:
{I}
,
es-E:
E
,
uall:
[x:A].
B[x]
,
top:
Top
,
set:
{x:A|
B[x]}
,
apply:
f
a
,
sqequal:
s
~
t
Definitions
:
uall:
[x:A].
B[x]
,
es-interface-predicate:
{I}
,
es-E-interface:
E(X)
,
member:
t
T
Lemmas
:
top_wf
\mforall{}[es,B,I:Top]. (\{e:E| \{I\} e\} \msim{} E(I))
Date html generated: 2011_08_16-PM-04_06_37
Last ObjectModification: 2011_06_20-AM-00_40_54
Home
Index
[x:A]. B[x], [es,B,I:Top]. ({e:E| {I} e} ~ E(I)) }[x:A]. B[x], [x:A]. B[x], 
T