---

Step * of Lemma cp-kinds_wf

∀[cp:ClassProgram(Top)]. (cp-kinds(cp) ∈ i:{i:Id| (i ∈ cp-domain(cp))}  ⟶ ({k:Knd| ↑hasloc(k;i)}  List))
BY
{ (Unfolds ``class-program cp-domain cp-kinds`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[cp:ClassProgram(Top)].  (cp-kinds(cp)  \mmember{}  i:\{i:Id|  (i  \mmember{}  cp-domain(cp))\}    {}\mrightarrow{}  (\{k:Knd|  \muparrow{}hasloc(k;i)\}    L\000Cist))


By

---

Latex:
(Unfolds  ``class-program  cp-domain  cp-kinds``  0  THEN  Auto)

---

Home Index