---

Step * of Lemma lnk-decl-dom-single

∀[l:IdLnk]. ∀[k:Knd]. ∀[tg:Id]. ∀[v:Top].  (k ∈ dom(lnk-decl(l;tg : v)) ~ rcv(l,tg) = k)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``lnk-decl fpf-dom fpf-single`` 0
   THEN Fold `eq_knd` 0
   THEN AutoBoolCase ⌜rcv(l,tg) = k⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[l:IdLnk].  \mforall{}[k:Knd].  \mforall{}[tg:Id].  \mforall{}[v:Top].    (k  \mmember{}  dom(lnk-decl(l;tg  :  v))  \msim{}  rcv(l,tg)  =  k)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``lnk-decl  fpf-dom  fpf-single``  0
  THEN  Fold  `eq\_knd`  0
  THEN  AutoBoolCase  \mkleeneopen{}rcv(l,tg)  =  k\mkleeneclose{}\mcdot{})

---

Home Index