---

Step * of Lemma es-decl-set-single_wf

∀[i:Id]. ∀[ds:x:Id fp-> Type]. ∀[da:k:{k:Knd| ↑hasloc(k;i)}  fp-> Type].  (es-decl-set-single(i;ds;da) ∈ DeclSet)
BY
{ (Unfolds ``es-decl-set es-decl-set-single`` 0 THEN Auto) }

1
1. i : Id
2. ds : x:Id fp-> Type
3. da : k:{k:Knd| ↑hasloc(k;i)}  fp-> Type
4. ∀i@0:Id. ((i@0 ∈ [i]) ∈ Type)
5. i1 : Id@i
6. (i1 ∈ [i])@i
⊢ da ∈ k:{k:Knd| ↑hasloc(k;i1)}  fp-> Type

---

Latex:

---

Latex:
\mforall{}[i:Id].  \mforall{}[ds:x:Id  fp->  Type].  \mforall{}[da:k:\{k:Knd|  \muparrow{}hasloc(k;i)\}    fp->  Type].
    (es-decl-set-single(i;ds;da)  \mmember{}  DeclSet)


By

---

Latex:
(Unfolds  ``es-decl-set  es-decl-set-single``  0  THEN  Auto)

---

Home Index