---

Step * of Lemma es-decl-set-ds_wf

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

---

Latex:


\mforall{}[dd:DeclSet].  \mforall{}[i:Id].    ds(dd;i)  \mmember{}  x:Id  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-ds``  0
  THEN  Auto)\mcdot{}

---

Home Index