---

Step * of Lemma C_Struct_wf

∀[fields:(Atom × C_TYPE()) List]. (C_Struct(fields) ∈ C_TYPE())
BY
{ DepprodCoDatatypeConstructorWf `C_TYPE_size` }

---

Latex:


\mforall{}[fields:(Atom  \mtimes{}  C\_TYPE())  List].  (C\_Struct(fields)  \mmember{}  C\_TYPE())


By

DepprodCoDatatypeConstructorWf  `C\_TYPE\_size`

---

Home Index