---

Step * 1 of Lemma es-dt-cap


1. da : k:Knd fp-> Type
2. l : IdLnk
3. tg : Id
4. T : Top
⊢ dt(l;da)(tg)?T ~ da(rcv(l,tg))?T
BY
{ (Unfold `fpf-cap` 0 THEN EqCD THEN Try (Trivial)) }

1
1. da : k:Knd fp-> Type
2. l : IdLnk
3. tg : Id
4. T : Top
⊢ tg ∈ dom(dt(l;da)) ~ rcv(l,tg) ∈ dom(da)

2
1. da : k:Knd fp-> Type
2. l : IdLnk
3. tg : Id
4. T : Top
⊢ dt(l;da)(tg) ~ da(rcv(l,tg))

---

Latex:



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


By

(Unfold  `fpf-cap`  0  THEN  EqCD  THEN  Try  (Trivial))

---

Home Index