---

Step * of Lemma lnk-decl-dom

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[tg:Id].  (rcv(l,tg) ∈ dom(lnk-decl(l;dt)) ~ tg ∈ dom(dt))
BY
{ ((UnivCD THENA Auto) THEN D 2 THEN Unfolds ``lnk-decl fpf-dom`` 0 THEN Reduce 0 THEN Auto) }

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

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[tg:Id].    (rcv(l,tg)  \mmember{}  dom(lnk-decl(l;dt))  \msim{}  tg  \mmember{}  dom(dt))


By

((UnivCD  THENA  Auto)  THEN  D  2  THEN  Unfolds  ``lnk-decl  fpf-dom``  0  THEN  Reduce  0  THEN  Auto)

---

Home Index