---

{ [i:Id]. [ds:x:Id fp-> Type]. [da:k:{k:Knd| hasloc(k;i)}  fp-> Type].
    (es-decl-set-single(i;ds;da)  DeclSet) }

{ Proof }

---

Definitions occuring in Statement :  es-decl-set-single: es-decl-set-single(i;ds;da),  es-decl-set: DeclSet,  fpf: a:A fp-> B[a],  hasloc: hasloc(k;i),  Knd: Knd,  Id: Id,  assert: b,  uall: [x:A]. B[x],  member: t  T,  set: {x:A| B[x]} ,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-decl-set: DeclSet,  es-decl-set-single: es-decl-set-single(i;ds;da),  prop: ,  so_lambda: x.t[x],  Id: Id,  so_apply: x[s],  implies: P  Q,  iff: P  Q,  all: x:A. B[x],  and: P  Q,  sq_type: SQType(T),  uimplies: b supposing a,  guard: {T}
Lemmas :  Id_wf,  l_member_wf,  fpf_wf,  Knd_wf,  assert_wf,  hasloc_wf,  member_singleton,  subtype_base_sq,  atom2_subtype_base

---

\mforall{}[i:Id].  \mforall{}[ds:x:Id  fp->  Type].  \mforall{}[da:k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type].
    (es-decl-set-single(i;ds;da)  \mmember{}  DeclSet)


Date html generated: 2011_08_16-AM-10_55_14
Last ObjectModification: 2011_06_18-AM-09_28_22

Home Index