---

{ [T:Type]. [P:i:Id  k:{k:Knd| hasloc(k;i)}   T]. [ik:LocKnd].
    (let i,k:LocKnd = ik in P[i;k]  T) }

{ Proof }

---

Definitions occuring in Statement :  locknd-spread: let i,k:LocKnd = ik in P[i; k],  LocKnd: LocKnd,  hasloc: hasloc(k;i),  Knd: Knd,  Id: Id,  assert: b,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  member: t  T,  set: {x:A| B[x]} ,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  LocKnd: LocKnd,  member: t  T,  locknd-spread: let i,k:LocKnd = ik in P[i; k],  so_apply: x[s1;s2],  implies: P  Q,  iff: P  Q,  prop: ,  and: P  Q,  rev_implies: P  Q
Lemmas :  assert_wf,  hasloc_wf,  Id_wf,  Knd_wf

---

\mforall{}[T:Type].  \mforall{}[P:i:Id  {}\mrightarrow{}  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    {}\mrightarrow{}  T].  \mforall{}[ik:LocKnd].
    (let  i,k:LocKnd  =  ik  in  P[i;k]  \mmember{}  T)


Date html generated: 2011_08_10-AM-07_51_55
Last ObjectModification: 2011_06_18-AM-08_14_17

Home Index