---

Step * 2 2 of Lemma lnk-decl-cap2

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

---

Latex:


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


By

Auto

---

Home Index