---

Step * of Lemma DVp_Array_wf

∀[lower,upper:ℤ]. ∀[arr:{lower..upper-} ─→ C_DVALUEp()].  (DVp_Array(lower;upper;arr) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }

---

Latex:


\mforall{}[lower,upper:\mBbbZ{}].  \mforall{}[arr:\{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp()].    (DVp\_Array(lower;upper;arr)  \mmember{}  C\_DVALUEp())


By

DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`

---

Home Index