---

Step * of Lemma es-tags-dt_wf

∀[l:IdLnk]. ∀[tgs:Id List]. ∀[da:k:Knd fp-> Type].  (dt(l;tgs;da) ∈ tg:Id fp-> Type)
BY
{ (Unfold `es-tags-dt` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:IdLnk].  \mforall{}[tgs:Id  List].  \mforall{}[da:k:Knd  fp->  Type].    (dt(l;tgs;da)  \mmember{}  tg:Id  fp->  Type)


By

---

Latex:
(Unfold  `es-tags-dt`  0  THEN  Auto)

---

Home Index