---

Step * of Lemma C_Array_wf

∀[length:ℕ]. ∀[elems:C_TYPE()].  (C_Array(length;elems) ∈ C_TYPE())
BY
{ DepprodCoDatatypeConstructorWf `C_TYPE_size` }

---

Latex:

---

Latex:
\mforall{}[length:\mBbbN{}].  \mforall{}[elems:C\_TYPE()].    (C\_Array(length;elems)  \mmember{}  C\_TYPE())


By

---

Latex:
DepprodCoDatatypeConstructorWf  `C\_TYPE\_size`

---

Home Index