---

Step * of Lemma es-decl-set-da_wf

∀[dd:DeclSet]. ∀[i:Id].  da(dd;i) ∈ k:{k:Knd| ↑hasloc(k;i)}  fp-> Type supposing (i ∈ |dd|)
BY
{ (Auto THEN RepeatFor 2 (D -3) THEN RepUR ``es-decl-set-domain`` -1 THEN RepUR ``es-decl-set-da`` 0 THEN Auto) }

---

Latex:


\mforall{}[dd:DeclSet].  \mforall{}[i:Id].    da(dd;i)  \mmember{}  k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type  supposing  (i  \mmember{}  |dd|)


By

(Auto
  THEN  RepeatFor  2  (D  -3)
  THEN  RepUR  ``es-decl-set-domain``  -1
  THEN  RepUR  ``es-decl-set-da``  0
  THEN  Auto)

---

Home Index