---

Step * 2 2 1 of Lemma lnk-decl_wf-hasloc


1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. k : Knd@i
4. ↑hasloc(k;destination(l))@i
5. y : Id
6. (y ∈ fst(dt))
7. k = rcv(l,y) ∈ {k:Knd| ↑hasloc(k;destination(l))} 
⊢ dt(snd(outl(rcv(l,y)))) ∈ Type
BY
{ (RepUR ``rcv fpf-ap`` 0⋅ THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  dt  :  d:Id  List  \mtimes{}  (tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type)
3.  k  :  Knd@i
4.  \muparrow{}hasloc(k;destination(l))@i
5.  y  :  Id
6.  (y  \mmember{}  fst(dt))
7.  k  =  rcv(l,y)
\mvdash{}  dt(snd(outl(rcv(l,y))))  \mmember{}  Type


By

(RepUR  ``rcv  fpf-ap``  0\mcdot{}  THEN  Auto)

---

Home Index