---

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


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

---

Latex:



1.  l  :  IdLnk
2.  dt  :  tg:Id  fp->  Type
3.  knd  :  Knd
4.  T  :  Type
5.  (\muparrow{}isrcv(knd))  {}\mRightarrow{}  (\muparrow{}lnk(knd)  =  l)  {}\mRightarrow{}  (\muparrow{}tag(knd)  \mmember{}  dom(dt))  {}\mRightarrow{}  (T  =  dt(tag(knd)))
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

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

---

Home Index