---

Step * 1 1 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 ∈ map(λtg.rcv(l,tg);fst(dt)))
8. x = knd ∈ Knd
⊢ dt(tag(knd)) = T ∈ Type
BY
{ ((All (Unfold `fpf-cap`)) THEN (All (Unfold `fpf-ap`)) THEN D 2 THEN All Reduce) }

1
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. (x ∈ map(λtg.rcv(l,tg);d))
9. x = knd ∈ Knd
⊢ (d1 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.  (x  \mmember{}  map(\mlambda{}tg.rcv(l,tg);fst(dt)))
8.  x  =  knd
\mvdash{}  dt(tag(knd))  =  T


By

((All  (Unfold  `fpf-cap`))  THEN  (All  (Unfold  `fpf-ap`))  THEN  D  2  THEN  All  Reduce)

---

Home Index