---

Step * 1 1 1 1 1 of Lemma lnk-decl-compatible-single


1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. knd : Knd
5. T : Type
6. (↑isrcv(knd)) ⇒ (↑lnk(knd) = l) ⇒ (↑tag(knd) ∈ dom(<d, d1>)) ⇒ (T = (d1 tag(knd)) ∈ Type)
7. x : Knd@i
8. y : Id
9. (y ∈ d)
10. x = rcv(l,y) ∈ Knd
11. x = knd ∈ Knd
⊢ (d1 tag(knd)) = T ∈ Type
BY
{ D 6 }

1
.....antecedent..... 
1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. knd : Knd
5. T : Type
6. x : Knd@i
7. y : Id
8. (y ∈ d)
9. x = rcv(l,y) ∈ Knd
10. x = knd ∈ Knd
⊢ ↑isrcv(knd)

2
1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. knd : Knd
5. T : Type
6. x : Knd@i
7. y : Id
8. (y ∈ d)
9. x = rcv(l,y) ∈ Knd
10. x = knd ∈ Knd
11. (↑lnk(knd) = l) ⇒ (↑tag(knd) ∈ dom(<d, d1>)) ⇒ (T = (d1 tag(knd)) ∈ Type)
⊢ (d1 tag(knd)) = T ∈ Type

---

Latex:



1.  l  :  IdLnk
2.  d  :  Id  List
3.  d1  :  tg:\{tg:Id|  (tg  \mmember{}  d)\}    {}\mrightarrow{}  Type
4.  knd  :  Knd
5.  T  :  Type
6.  (\muparrow{}isrcv(knd))  {}\mRightarrow{}  (\muparrow{}lnk(knd)  =  l)  {}\mRightarrow{}  (\muparrow{}tag(knd)  \mmember{}  dom(<d,  d1>))  {}\mRightarrow{}  (T  =  (d1  tag(knd)))
7.  x  :  Knd@i
8.  y  :  Id
9.  (y  \mmember{}  d)
10.  x  =  rcv(l,y)
11.  x  =  knd
\mvdash{}  (d1  tag(knd))  =  T


By

D  6

---

Home Index