---

Step * of Lemma C_Pointer-to_wf

∀[v:C_TYPE()]. C_Pointer-to(v) ∈ C_TYPE() supposing ↑C_Pointer?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:C\_TYPE()].  C\_Pointer-to(v)  \mmember{}  C\_TYPE()  supposing  \muparrow{}C\_Pointer?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index