---

Step * of Lemma DVp_Null-x_wf

∀[v:C_DVALUEp()]. DVp_Null-x(v) ∈ Unit supposing ↑DVp_Null?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:C\_DVALUEp()].  DVp\_Null-x(v)  \mmember{}  Unit  supposing  \muparrow{}DVp\_Null?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index