---

Step * 1 2 1 of Lemma lnk-decl-cap


1. l : IdLnk
2. dt : tg:Id fp-> Type
3. tg : Id
4. T : Type
5. ↑rcv(l,tg) ∈ dom(lnk-decl(l;dt))
⊢ ↑tg ∈ dom(dt)
BY
{ (D 2 THEN (All (\h. (Unfolds ``lnk-decl fpf-dom`` h THEN Reduce h THEN RWO "assert-deq-member" h THEN Auto)))⋅) }

1
1. l : IdLnk
2. d : Id List
3. d1 : tg:{tg:Id| (tg ∈ d)}  ─→ Type
4. tg : Id
5. T : Type
6. (rcv(l,tg) ∈ map(λtg.rcv(l,tg);d))
⊢ (tg ∈ d)

---

Latex:



1.  l  :  IdLnk
2.  dt  :  tg:Id  fp->  Type
3.  tg  :  Id
4.  T  :  Type
5.  \muparrow{}rcv(l,tg)  \mmember{}  dom(lnk-decl(l;dt))
\mvdash{}  \muparrow{}tg  \mmember{}  dom(dt)


By

(D  2
  THEN  (All  (\mbackslash{}h.  (Unfolds  ``lnk-decl  fpf-dom``  h
                                  THEN  Reduce  h
                                  THEN  RWO  "assert-deq-member"  h
                                  THEN  Auto)))\mcdot{}
  )

---

Home Index