---

Step * of Lemma DVp_Array-arr_wf

∀[v:C_DVALUEp()]. DVp_Array-arr(v) ∈ {DVp_Array-lower(v)..DVp_Array-upper(v)-} ─→ C_DVALUEp() supposing ↑DVp_Array?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[v:C\_DVALUEp()]
    DVp\_Array-arr(v)  \mmember{}  \{DVp\_Array-lower(v)..DVp\_Array-upper(v)\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp() 
    supposing  \muparrow{}DVp\_Array?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index