---

Step * 1 of Lemma es-dt_wf


1. l : IdLnk
2. da : k:Knd fp-> Type
3. y : Knd@i
4. ↑isrcv(y)
5. lnk(y) = l ∈ IdLnk
6. True@i
⊢ rcv(l,tag(y)) = y ∈ Knd
BY
{ RepeatFor 2 ((D 3 THEN All (RepUR ``isrcv lnk tagof rcv Knd``)  THEN Auto)) }

---

Latex:



1.  l  :  IdLnk
2.  da  :  k:Knd  fp->  Type
3.  y  :  Knd@i
4.  \muparrow{}isrcv(y)
5.  lnk(y)  =  l
6.  True@i
\mvdash{}  rcv(l,tag(y))  =  y


By

RepeatFor  2  ((D  3  THEN  All  (RepUR  ``isrcv  lnk  tagof  rcv  Knd``)    THEN  Auto))

---

Home Index