---

Step * of Lemma C_Void_wf

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

---

Latex:


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


By

DepprodCoDatatypeConstructorWf  `C\_TYPE\_size`

---

Home Index