---

Step * of Lemma lnk-decl_wf

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type].  (lnk-decl(l;dt) ∈ k:Knd 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. ∀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

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].    (lnk-decl(l;dt)  \mmember{}  k:Knd  fp->  Type)


By

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

---

Home Index