---

Step * of Lemma C_Int_wf

C_Int() ∈ C_TYPE()
BY
{ DepprodCoDatatypeConstructorWf `C_TYPE_size` }

---

Latex:

---

Latex:
C\_Int()  \mmember{}  C\_TYPE()


By

---

Latex:
DepprodCoDatatypeConstructorWf  `C\_TYPE\_size`

---

Home Index