---

Step * of Lemma C_DVALUEp_size_wf

∀[p:C_DVALUEp()]. (C_DVALUEp_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `C_DVALUEpco_size` }

---

Latex:


\mforall{}[p:C\_DVALUEp()].  (C\_DVALUEp\_size(p)  \mmember{}  \mBbbN{})


By

ProveCoSizeWf2  `C\_DVALUEpco\_size`

---

Home Index