---

Step * 1 1 1 1 3 1 of Lemma es-dt-dom

.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. (rcv(l,tg) ∈ fpf-domain(da))@i
⊢ rcv(l,tg) ∈ Knd
BY
{ Auto }

---

Latex:


.....wf..... 
1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
4.  (rcv(l,tg)  \mmember{}  fpf-domain(da))@i
\mvdash{}  rcv(l,tg)  \mmember{}  Knd


By

Auto

---

Home Index