{ 
[dd:DeclSet]. 
[i:Id].
    da(dd;i) 
 k:{k:Knd| 
hasloc(k;i)}  fp-> Type supposing (i 
 |dd|) }
{ Proof }
Definitions occuring in Statement : 
es-decl-set-da: da(dd;i), 
es-decl-set-domain: |dd|, 
es-decl-set: DeclSet, 
fpf: a:A fp-> B[a], 
hasloc: hasloc(k;i), 
Knd: Knd, 
Id: Id, 
assert:
b, 
uimplies: b supposing a, 
uall:
[x:A]. B[x], 
member: t 
 T, 
set: {x:A| B[x]} , 
universe: Type, 
l_member: (x 
 l)
Definitions : 
uall:
[x:A]. B[x], 
uimplies: b supposing a, 
member: t 
 T, 
es-decl-set-da: da(dd;i), 
pi2: snd(t), 
es-decl-set: DeclSet, 
es-decl-set-domain: |dd|, 
pi1: fst(t), 
prop:
Lemmas : 
l_member_wf, 
Id_wf, 
es-decl-set-domain_wf, 
es-decl-set_wf
\mforall{}[dd:DeclSet].  \mforall{}[i:Id].    da(dd;i)  \mmember{}  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type  supposing  (i  \mmember{}  |dd|)
Date html generated:
2011_08_16-AM-10_55_30
Last ObjectModification:
2011_06_18-AM-09_28_38
Home
Index