---

Step * of Lemma DVp_Null_wf

∀[x:Unit]. (DVp_Null(x) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }

---

Latex:


\mforall{}[x:Unit].  (DVp\_Null(x)  \mmember{}  C\_DVALUEp())


By

DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`

---

Home Index