---

Step * of Lemma lnk-decl_wf-hasloc

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type].  (lnk-decl(l;dt) ∈ k:{k:Knd| ↑hasloc(k;destination(l))}  fp-> Type)
BY
{ (Unfolds ``fpf lnk-decl`` 0 THEN Auto) }

1
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. tg : Id@i
⊢ rcv(l,tg) ∈ {k:Knd| ↑hasloc(k;destination(l))} 

2
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. k : {k:{k:Knd| ↑hasloc(k;destination(l))} | (k ∈ map(λtg.rcv(l,tg);fst(dt)))} @i
⊢ dt(snd(outl(k))) ∈ Type

3
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. ∀k:Knd. (↑hasloc(k;destination(l)) ∈ Type)
4. k : Knd
5. ↑hasloc(k;destination(l))
6. tg : Id@i
⊢ rcv(l,tg) ∈ {k:Knd| ↑hasloc(k;destination(l))} 

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].    (lnk-decl(l;dt)  \mmember{}  k:\{k:Knd|  \muparrow{}hasloc(k;destination(l))\}    fp->  Typ\000Ce)


By

(Unfolds  ``fpf  lnk-decl``  0  THEN  Auto)

---

Home Index