---

Step * of Lemma DVp_Int_wf

∀[int:ℤ]. (DVp_Int(int) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }

---

Latex:

---

Latex:
\mforall{}[int:\mBbbZ{}].  (DVp\_Int(int)  \mmember{}  C\_DVALUEp())


By

---

Latex:
DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`

---

Home Index