---

Step * 1 of Lemma es-dt-dom


∀l:IdLnk. ∀da:k:Knd fp-> Type. ∀tg:Id.  (↑tg ∈ dom(dt(l;da)) ⇐⇒ ↑rcv(l,tg) ∈ dom(da))
BY
{ (UnivCD THENA Auto) }

1
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
⊢ ↑tg ∈ dom(dt(l;da)) ⇐⇒ ↑rcv(l,tg) ∈ dom(da)

---

Latex:



\mforall{}l:IdLnk.  \mforall{}da:k:Knd  fp->  Type.  \mforall{}tg:Id.    (\muparrow{}tg  \mmember{}  dom(dt(l;da))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}rcv(l,tg)  \mmember{}  dom(da))


By

(UnivCD  THENA  Auto)

---

Home Index