---

Step * of Lemma pDVselex_wf

∀[rndv1:ℕ × Id × ℕ × Name]. (pDVselex(rndv1) ∈ PiDataVal())
BY
{ Unfolds ``PiDataVal pDVselex`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[rndv1:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name].  (pDVselex(rndv1)  \mmember{}  PiDataVal())


By

---

Latex:
Unfolds  ``PiDataVal  pDVselex``  0  THEN  Auto  THEN  MemTypeCD  THEN  Auto

---

Home Index