---

Step * 1 2 of Lemma lnk-decl-cap

.....falsecase..... 
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. tg : Id
4. T : Type
5. ↑rcv(l,tg) ∈ dom(lnk-decl(l;dt))
6. ¬↑tg ∈ dom(dt)
⊢ lnk-decl(l;dt)(rcv(l,tg)) ~ T
BY
{ D (-1) }

1
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. tg : Id
4. T : Type
5. ↑rcv(l,tg) ∈ dom(lnk-decl(l;dt))
⊢ ↑tg ∈ dom(dt)

---

Latex:


.....falsecase..... 
1.  l  :  IdLnk
2.  dt  :  tg:Id  fp->  Type
3.  tg  :  Id
4.  T  :  Type
5.  \muparrow{}rcv(l,tg)  \mmember{}  dom(lnk-decl(l;dt))
6.  \mneg{}\muparrow{}tg  \mmember{}  dom(dt)
\mvdash{}  lnk-decl(l;dt)(rcv(l,tg))  \msim{}  T


By

D  (-1)

---

Home Index