---

Step * of Lemma C_Array-length_wf

∀[v:C_TYPE()]. C_Array-length(v) ∈ ℕ supposing ↑C_Array?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[v:C\_TYPE()].  C\_Array-length(v)  \mmember{}  \mBbbN{}  supposing  \muparrow{}C\_Array?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index