---

Step * of Lemma pDVmsg_wf

∀[val:Name]. ∀[index:ℕ].  (pDVmsg(val;index) ∈ PiDataVal())
BY
{ Unfolds ``PiDataVal pDVmsg`` 0 THEN Auto THEN MemTypeCD THEN Auto }

---

Latex:

---

Latex:
\mforall{}[val:Name].  \mforall{}[index:\mBbbN{}].    (pDVmsg(val;index)  \mmember{}  PiDataVal())


By

---

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

---

Home Index