---

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


1. l : IdLnk
2. dt : tg:Id fp-> Type
3. knd : Knd
4. T : Type
5. (↑isrcv(knd)) ⇒ (lnk(knd) = l ∈ IdLnk) ⇒ (T = dt(tag(knd))?Void ∈ Type)
6. x : Knd@i
7. ↑x ∈ dom(lnk-decl(l;dt))@i
8. x = knd ∈ Knd
⊢ lnk-decl(l;dt)(knd) = T ∈ Type
BY
{ (Unfolds ``lnk-decl fpf-ap fpf-single`` 0 THEN Reduce 0 THEN Fold `tagof` 0) }

1
1. l : IdLnk
2. dt : tg:Id fp-> Type
3. knd : Knd
4. T : Type
5. (↑isrcv(knd)) ⇒ (lnk(knd) = l ∈ IdLnk) ⇒ (T = dt(tag(knd))?Void ∈ Type)
6. x : Knd@i
7. ↑x ∈ dom(lnk-decl(l;dt))@i
8. x = knd ∈ Knd
⊢ dt(tag(knd)) = T ∈ Type

---

Latex:

---

Latex:

1.  l  :  IdLnk
2.  dt  :  tg:Id  fp->  Type
3.  knd  :  Knd
4.  T  :  Type
5.  (\muparrow{}isrcv(knd))  {}\mRightarrow{}  (lnk(knd)  =  l)  {}\mRightarrow{}  (T  =  dt(tag(knd))?Void)
6.  x  :  Knd@i
7.  \muparrow{}x  \mmember{}  dom(lnk-decl(l;dt))@i
8.  x  =  knd
\mvdash{}  lnk-decl(l;dt)(knd)  =  T


By

---

Latex:
(Unfolds  ``lnk-decl  fpf-ap  fpf-single``  0  THEN  Reduce  0  THEN  Fold  `tagof`  0)

---

Home Index