{ 
[dd1,dd2:DeclSet]. (dd1 
dd2 
') }
{ Proof }
Definitions occuring in Statement :
es-decl-sets-sub: dd1 dd2,
es-decl-set: DeclSet,
uall: [x:A]. B[x],
prop: ,
member: t T
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
es-decl-sets-sub: dd1 dd2,
spreadn: spread3,
all: x:A. B[x],
implies: P 
Q,
and: P 
Q,
cand: A c B,
so_lambda: 
x.t[x],
es-decl-set: DeclSet,
so_apply: x[s],
uimplies: b supposing a
Lemmas :
Id_wf,
l_member_wf,
fpf-sub_wf,
Knd_wf,
assert_wf,
hasloc_wf,
Kind-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
id-deq_wf,
es-decl-set_wf
\mforall{}[dd1,dd2:DeclSet]. (dd1 \msubseteq{} dd2 \mmember{} \mBbbP{}')
Date html generated:
2011_08_16-AM-10_56_07
Last ObjectModification:
2011_06_18-AM-09_29_18
Home
Index