---

Step * of Lemma C_Int_wf

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

---

Latex:


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


By

DepprodCoDatatypeConstructorWf  `C\_TYPE\_size`

---

Home Index