---

Step * 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 ∈ dom(lnk-decl(l;dt))@i
8. x = knd ∈ Knd
⊢ dt(tag(knd)) = T ∈ Type
BY
{ (((Unfolds ``fpf-dom lnk-decl`` (-2)) THEN (Reduce (-2)) THEN (RWO "assert-deq-member" (-2))) THENA Auto) }

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 ∈ map(λtg.rcv(l,tg);fst(dt)))
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{}  dt(tag(knd))  =  T


By

(((Unfolds  ``fpf-dom  lnk-decl``  (-2))  THEN  (Reduce  (-2))  THEN  (RWO  "assert-deq-member"  (-2)))
  THENA  Auto
  )

---

Home Index