---

Step * 1 2 of Lemma es-dt-cap


1. da : k:Knd fp-> Type
2. l : IdLnk
3. tg : Id
4. T : Top
⊢ dt(l;da)(tg) ~ da(rcv(l,tg))
BY
{ (DVar `da' THEN RepUR ``es-dt compose-fpf fpf-cap fpf-domain fpf-dom fpf-ap`` 0 THEN Trivial) }

---

Latex:



1.  da  :  k:Knd  fp->  Type
2.  l  :  IdLnk
3.  tg  :  Id
4.  T  :  Top
\mvdash{}  dt(l;da)(tg)  \msim{}  da(rcv(l,tg))


By

(DVar  `da'  THEN  RepUR  ``es-dt  compose-fpf  fpf-cap  fpf-domain  fpf-dom  fpf-ap``  0  THEN  Trivial)

---

Home Index