---

Step * 1 of Lemma lnk-decl_wf


1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. ∀k:Knd. ((k ∈ map(λtg.rcv(l,tg);fst(dt))) ∈ Type)
4. k : Knd@i
5. (k ∈ map(λtg.rcv(l,tg);fst(dt)))@i
⊢ dt(snd(outl(k))) ∈ Type
BY
{ (((RWO "member_map" (-1)) THENA Auto) THEN (Reduce (-1)) THEN ExRepD THEN (HypSubst' (-1) 0)) }

1
1. l : IdLnk
2. dt : d:Id List × (tg:{tg:Id| (tg ∈ d)}  ─→ Type)
3. ∀k:Knd. ((k ∈ map(λtg.rcv(l,tg);fst(dt))) ∈ Type)
4. k : Knd@i
5. y : Id
6. (y ∈ fst(dt))
7. k = rcv(l,y) ∈ Knd
⊢ dt(snd(outl(rcv(l,y)))) ∈ Type

---

Latex:



1.  l  :  IdLnk
2.  dt  :  d:Id  List  \mtimes{}  (tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type)
3.  \mforall{}k:Knd.  ((k  \mmember{}  map(\mlambda{}tg.rcv(l,tg);fst(dt)))  \mmember{}  Type)
4.  k  :  Knd@i
5.  (k  \mmember{}  map(\mlambda{}tg.rcv(l,tg);fst(dt)))@i
\mvdash{}  dt(snd(outl(k)))  \mmember{}  Type


By

(((RWO  "member\_map"  (-1))  THENA  Auto)  THEN  (Reduce  (-1))  THEN  ExRepD  THEN  (HypSubst'  (-1)  0))

---

Home Index