---

Step * of Lemma lnk-decl-dom-not

∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[a:Id].  (locl(a) ∈ dom(lnk-decl(l;dt)) ~ ff)
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. a : Id
⊢ locl(a) ∈b map(λtg.rcv(l,tg);d)) = ff

---

Latex:


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


By

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

---

Home Index