---

Step * 2 1 of Lemma lnk-decl-cap2

.....truecase..... 
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))
⊢ lnk-decl(l1;dt)(rcv(l2,tg)) ~ T
BY
{ ((FLemma `lnk-decl-dom2` [(-1)]) THEN Auto) }

---

Latex:


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


By

((FLemma  `lnk-decl-dom2`  [(-1)])  THEN  Auto)

---

Home Index