---

Step * 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
⊢ lnk-decl(l1;dt)(rcv(l2,tg))?T ~ dt(tg)?T
BY
{ ((HypSubst' (-1) 0) THEN RWO "lnk-decl-cap" 0 THEN Auto) }

---

Latex:


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


By

((HypSubst'  (-1)  0)  THEN  RWO  "lnk-decl-cap"  0  THEN  Auto)

---

Home Index