---

Step * 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)
⊢ lnk-decl(l1;dt)(rcv(l2,tg))?T ~ T
BY
{ ((Unfold `fpf-cap` 0 THEN SplitOnConclITE) THENA Auto) }

1
.....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

2
.....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

---

Latex:


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


By

((Unfold  `fpf-cap`  0  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index